equal
deleted
inserted
replaced
1045 hypreal_zero_def,FreeUltrafilterNat_Nat_set])); |
1045 hypreal_zero_def,FreeUltrafilterNat_Nat_set])); |
1046 qed "hypreal_of_real_zero_iff"; |
1046 qed "hypreal_of_real_zero_iff"; |
1047 |
1047 |
1048 Goal "hypreal_of_real (inverse r) = inverse (hypreal_of_real r)"; |
1048 Goal "hypreal_of_real (inverse r) = inverse (hypreal_of_real r)"; |
1049 by (case_tac "r=0" 1); |
1049 by (case_tac "r=0" 1); |
1050 by (asm_simp_tac (simpset() addsimps [REAL_DIVIDE_ZERO, INVERSE_ZERO, |
1050 by (asm_simp_tac (simpset() addsimps [DIVISION_BY_ZERO, INVERSE_ZERO, |
1051 HYPREAL_INVERSE_ZERO]) 1); |
1051 HYPREAL_INVERSE_ZERO]) 1); |
1052 by (res_inst_tac [("c1","hypreal_of_real r")] |
1052 by (res_inst_tac [("c1","hypreal_of_real r")] |
1053 (hypreal_mult_left_cancel RS iffD1) 1); |
1053 (hypreal_mult_left_cancel RS iffD1) 1); |
1054 by (stac (hypreal_of_real_mult RS sym) 2); |
1054 by (stac (hypreal_of_real_mult RS sym) 2); |
1055 by (auto_tac (claset(), simpset() addsimps [hypreal_of_real_zero_iff])); |
1055 by (auto_tac (claset(), simpset() addsimps [hypreal_of_real_zero_iff])); |