changeset 19758 | 093690d4ba60 |
parent 19757 | 4a2a71c31968 |
child 22810 | a8455ca995d6 |
--- a/src/LCF/LCF.thy Thu Jun 01 23:07:51 2006 +0200 +++ b/src/LCF/LCF.thy Thu Jun 01 23:09:34 2006 +0200 @@ -370,7 +370,8 @@ shows "P(FIX(f),FIX(g))" apply (rule FIX1 [THEN ssubst, of _ f g]) apply (rule FIX2 [THEN ssubst, of _ f g]) - apply (rule induct [OF 1, where ?f = "%x. <f(FST(x)),g(SND(x))>"]) + apply (rule induct [where ?f = "%x. <f(FST(x)),g(SND(x))>"]) + apply (rule 1) apply simp apply (rule 2) apply (simp add: expand_all_PROD)