| changeset 18447 | da548623916a |
| parent 18242 | 2215049cd29c |
| child 18460 | 9a1458cb2956 |
--- a/src/HOL/Induct/QuoNestedDataType.thy Tue Dec 20 22:06:00 2005 +0100 +++ b/src/HOL/Induct/QuoNestedDataType.thy Wed Dec 21 12:02:57 2005 +0100 @@ -222,7 +222,7 @@ lemma ExpList_rep: "\<exists>Us. z = Abs_ExpList Us" apply (induct z) apply (rule_tac [2] z=a in eq_Abs_Exp) -apply (auto simp add: Abs_ExpList_def intro: exprel_refl) +apply (auto simp add: Abs_ExpList_def Cons_eq_map_conv intro: exprel_refl) done lemma eq_Abs_ExpList [case_names Abs_ExpList]: