equal
deleted
inserted
replaced
93 by (cut_inst_tac [("m","m")] less_linear 1); |
93 by (cut_inst_tac [("m","m")] less_linear 1); |
94 by (blast_tac (claset() addIs [Suc_mono]) 1); |
94 by (blast_tac (claset() addIs [Suc_mono]) 1); |
95 qed "Least_Suc"; |
95 qed "Least_Suc"; |
96 |
96 |
97 val prems = Goal "[| P 0; P 1; !!k. P k ==> P (Suc (Suc k)) |] ==> P n"; |
97 val prems = Goal "[| P 0; P 1; !!k. P k ==> P (Suc (Suc k)) |] ==> P n"; |
98 by (rtac less_induct 1); |
98 by (rtac nat_less_induct 1); |
99 by (case_tac "n" 1); |
99 by (case_tac "n" 1); |
100 by (case_tac "nat" 2); |
100 by (case_tac "nat" 2); |
101 by (ALLGOALS (blast_tac (claset() addIs prems@[less_trans]))); |
101 by (ALLGOALS (blast_tac (claset() addIs prems@[less_trans]))); |
102 qed "nat_induct2"; |
102 qed "nat_induct2"; |
103 |
103 |