changeset 5184 | 9b8547a9496a |
parent 5148 | 74919e8f221c |
child 5459 | 1dbaf888f4e7 |
--- a/src/HOL/Real/Real.ML Fri Jul 24 13:03:20 1998 +0200 +++ b/src/HOL/Real/Real.ML Fri Jul 24 13:19:38 1998 +0200 @@ -1267,7 +1267,7 @@ Goal "1r <= %%#n"; by (simp_tac (simpset() addsimps [real_nat_one RS sym]) 1); -by (nat_ind_tac "n" 1); +by (induct_tac "n" 1); by (auto_tac (claset(),simpset () addsimps [real_nat_Suc,real_le_refl,real_nat_one])); by (res_inst_tac [("t","1r")] (real_add_zero_left RS subst) 1);