equal
deleted
inserted
replaced
36 by (ALLGOALS (resolve_tac evalc.intrs THEN_ALL_NEW atac)); |
36 by (ALLGOALS (resolve_tac evalc.intrs THEN_ALL_NEW atac)); |
37 qed "evaln_evalc"; |
37 qed "evaln_evalc"; |
38 |
38 |
39 goal Nat.thy "(Suc n <= m') --> (? m. m' = Suc m)"; |
39 goal Nat.thy "(Suc n <= m') --> (? m. m' = Suc m)"; |
40 by (induct_tac "m'" 1); |
40 by (induct_tac "m'" 1); |
41 by Auto_tac; |
41 by (CLASIMPSET auto_tac); |
42 qed_spec_mp "Suc_le_D"; |
42 qed_spec_mp "Suc_le_D"; |
43 |
43 |
44 Goal "[| Suc n <= m'; (!!m. n <= m ==> P (Suc m)) |] ==> P m'"; |
44 Goal "[| Suc n <= m'; (!!m. n <= m ==> P (Suc m)) |] ==> P m'"; |
45 by (cut_facts_tac (premises()) 1); |
45 by (cut_facts_tac (premises()) 1); |
46 by (ftac Suc_le_D 1); |
46 by (ftac Suc_le_D 1); |