changeset 14275 | 031a5a051bb4 |
parent 14268 | 5cf13e80be0e |
--- a/src/HOL/Hyperreal/HyperDef.ML Thu Dec 04 21:57:15 2003 +0100 +++ b/src/HOL/Hyperreal/HyperDef.ML Fri Dec 05 10:28:02 2003 +0100 @@ -1047,7 +1047,7 @@ Goal "hypreal_of_real (inverse r) = inverse (hypreal_of_real r)"; by (case_tac "r=0" 1); -by (asm_simp_tac (simpset() addsimps [REAL_DIVIDE_ZERO, INVERSE_ZERO, +by (asm_simp_tac (simpset() addsimps [DIVISION_BY_ZERO, INVERSE_ZERO, HYPREAL_INVERSE_ZERO]) 1); by (res_inst_tac [("c1","hypreal_of_real r")] (hypreal_mult_left_cancel RS iffD1) 1);