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]: