diff -r 886655a150f6 -r d1b97708d5eb src/CCL/Fix.thy --- a/src/CCL/Fix.thy Thu Jun 21 20:48:48 2007 +0200 +++ b/src/CCL/Fix.thy Thu Jun 21 22:10:16 2007 +0200 @@ -181,9 +181,10 @@ done lemma term_ind: - assumes "P(bot)" "P(true)" "P(false)" - "!!x y.[| P(x); P(y) |] ==> P()" - "!!u.(!!x. P(u(x))) ==> P(lam x. u(x))" "INCL(P)" + assumes 1: "P(bot)" and 2: "P(true)" and 3: "P(false)" + and 4: "!!x y.[| P(x); P(y) |] ==> P()" + and 5: "!!u.(!!x. P(u(x))) ==> P(lam x. u(x))" + and 6: "INCL(P)" shows "P(t)" apply (rule reachability [THEN id_apply, THEN subst]) apply (rule_tac x = t in spec) @@ -191,12 +192,12 @@ apply (unfold idgen_def) apply (rule allI) apply (subst applyBbot) - apply assumption + apply (rule 1) apply (rule allI) apply (rule applyB [THEN ssubst]) apply (rule_tac t = "xa" in term_case) apply simp_all - apply (fast intro: prems INCL_subst all_INCL)+ + apply (fast intro: assms INCL_subst all_INCL)+ done end