QuotMain.thy
changeset 310 fec6301a1989
parent 307 9aa3aba71ecc
child 311 77fc6f3c0343
--- a/QuotMain.thy	Wed Nov 11 22:30:43 2009 +0100
+++ b/QuotMain.thy	Thu Nov 12 02:18:36 2009 +0100
@@ -137,7 +137,6 @@
 
 end
 
-
 section {* type definition for the quotient type *}
 
 (* the auxiliary data for the quotient types *)
@@ -160,6 +159,8 @@
 (* lifting of constants *)
 use "quotient_def.ML"
 
+
+
 section {* ATOMIZE *}
 
 lemma atomize_eqv[atomize]: