| changeset 55417 | 01fbfb60c33e |
| parent 49834 | b27bbb021df1 |
| child 58305 | 57752a91eec4 |
--- a/src/HOL/Induct/QuoNestedDataType.thy Wed Feb 12 08:35:57 2014 +0100 +++ b/src/HOL/Induct/QuoNestedDataType.thy Wed Feb 12 08:37:06 2014 +0100 @@ -212,6 +212,7 @@ lemma ExpList_rep: "\<exists>Us. z = Abs_ExpList Us" apply (induct z) +apply (rename_tac [2] a b) apply (rule_tac [2] z=a in eq_Abs_Exp) apply (auto simp add: Abs_ExpList_def Cons_eq_map_conv intro: exprel_refl) done