changeset 18242 | 2215049cd29c |
parent 16417 | 9bc16273c2d4 |
child 18447 | da548623916a |
--- a/src/HOL/Induct/QuoNestedDataType.thy Wed Nov 23 22:26:13 2005 +0100 +++ b/src/HOL/Induct/QuoNestedDataType.thy Thu Nov 24 00:00:20 2005 +0100 @@ -265,7 +265,7 @@ lemma listset_Rep_Exp_Abs_Exp: "listset (map Rep_Exp (Abs_ExpList Us)) = listrel exprel `` {Us}"; -by (induct_tac Us, simp_all add: listrel_Cons Abs_ExpList_def) +by (induct Us, simp_all add: listrel_Cons Abs_ExpList_def) lemma FnCall: "FnCall F (Abs_ExpList Us) = Abs_Exp (exprel``{FNCALL F Us})" @@ -459,4 +459,3 @@ qed end -