diff -r 20fa8dd8fb93 -r fec6301a1989 QuotMain.thy --- 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]: