Quot/Nominal/Abs.thy
changeset 1090 de2d1929899f
parent 1089 66097fe4942a
child 1096 a69ec3f3f535
--- a/Quot/Nominal/Abs.thy	Mon Feb 08 13:50:52 2010 +0100
+++ b/Quot/Nominal/Abs.thy	Tue Feb 09 10:48:42 2010 +0100
@@ -226,7 +226,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