| changeset 14275 | 031a5a051bb4 |
| parent 14270 | 342451d763f9 |
| child 14288 | d149e3cbdb39 |
--- a/src/HOL/Hyperreal/Lim.ML Thu Dec 04 21:57:15 2003 +0100 +++ b/src/HOL/Hyperreal/Lim.ML Fri Dec 05 10:28:02 2003 +0100 @@ -2043,7 +2043,7 @@ Goal "f a - (f b - f a)/(b - a) * a = \ \ f b - (f b - f a)/(b - a) * (b::real)"; by (case_tac "a = b" 1); -by (asm_full_simp_tac (simpset() addsimps [REAL_DIVIDE_ZERO]) 1); +by (asm_full_simp_tac (simpset() addsimps [DIVISION_BY_ZERO]) 1); by (res_inst_tac [("c1","b - a")] (real_mult_left_cancel RS iffD1) 1); by (arith_tac 1); by (auto_tac (claset(),