equal
deleted
inserted
replaced
1265 by (Blast_tac 1); |
1265 by (Blast_tac 1); |
1266 qed "real_nat_less_zero"; |
1266 qed "real_nat_less_zero"; |
1267 |
1267 |
1268 Goal "1r <= %%#n"; |
1268 Goal "1r <= %%#n"; |
1269 by (simp_tac (simpset() addsimps [real_nat_one RS sym]) 1); |
1269 by (simp_tac (simpset() addsimps [real_nat_one RS sym]) 1); |
1270 by (nat_ind_tac "n" 1); |
1270 by (induct_tac "n" 1); |
1271 by (auto_tac (claset(),simpset () |
1271 by (auto_tac (claset(),simpset () |
1272 addsimps [real_nat_Suc,real_le_refl,real_nat_one])); |
1272 addsimps [real_nat_Suc,real_le_refl,real_nat_one])); |
1273 by (res_inst_tac [("t","1r")] (real_add_zero_left RS subst) 1); |
1273 by (res_inst_tac [("t","1r")] (real_add_zero_left RS subst) 1); |
1274 by (rtac real_add_le_mono 1); |
1274 by (rtac real_add_le_mono 1); |
1275 by (auto_tac (claset(),simpset () |
1275 by (auto_tac (claset(),simpset () |