Quot/Nominal/Abs.thy
changeset 1096 a69ec3f3f535
parent 1095 8441b4b2469d
parent 1090 de2d1929899f
child 1128 17ca92ab4660
--- a/Quot/Nominal/Abs.thy	Tue Feb 09 15:20:40 2010 +0100
+++ b/Quot/Nominal/Abs.thy	Tue Feb 09 15:20:52 2010 +0100
@@ -227,7 +227,6 @@
 
 (* TEST case *)
 lemmas abs_induct2 = prod.induct[where 'a="atom set" and 'b="'a::pt", quot_lifted]
-
 thm abs_induct abs_induct2
 
 instantiation abs :: (pt) pt