changeset 49834 | b27bbb021df1 |
parent 45694 | 4a8743618257 |
child 55417 | 01fbfb60c33e |
--- a/src/HOL/Induct/QuoNestedDataType.thy Fri Oct 12 15:08:29 2012 +0200 +++ b/src/HOL/Induct/QuoNestedDataType.thy Fri Oct 12 18:58:20 2012 +0200 @@ -144,7 +144,7 @@ definition "Exp = UNIV//exprel" -typedef (open) exp = Exp +typedef exp = Exp morphisms Rep_Exp Abs_Exp unfolding Exp_def by (auto simp add: quotient_def)