equal
deleted
inserted
replaced
202 Addsimps [Suc_n_div_2_gt_zero]; |
202 Addsimps [Suc_n_div_2_gt_zero]; |
203 |
203 |
204 Goal "0 < n & even n --> 1 < n"; |
204 Goal "0 < n & even n --> 1 < n"; |
205 by (induct_tac "n" 1); |
205 by (induct_tac "n" 1); |
206 by Auto_tac; |
206 by Auto_tac; |
207 qed_spec_mp "even_gt_zero_gt_one"; |
207 qed_spec_mp "even_gt_zero_gt_one_aux"; |
208 bind_thm ("even_gt_zero_gt_one",conjI RS even_gt_zero_gt_one); |
208 bind_thm ("even_gt_zero_gt_one",conjI RS even_gt_zero_gt_one_aux); |
209 |
209 |
210 (* more general *) |
210 (* more general *) |
211 Goal "n div 2 <= (Suc n) div 2"; |
211 Goal "n div 2 <= (Suc n) div 2"; |
212 by (arith_tac 1); |
212 by (arith_tac 1); |
213 qed "le_Suc_n_div_2"; |
213 qed "le_Suc_n_div_2"; |