src/HOL/Hyperreal/HyperDef.thy
changeset 14334 6137d24eef79
parent 14331 8dbbb7cf3637
child 14341 a09441bd4f1e
     1.1 --- a/src/HOL/Hyperreal/HyperDef.thy	Mon Dec 29 06:49:26 2003 +0100
     1.2 +++ b/src/HOL/Hyperreal/HyperDef.thy	Thu Jan 01 10:06:32 2004 +0100
     1.3 @@ -326,7 +326,7 @@
     1.4  lemma hypreal_add_commute: "(z::hypreal) + w = w + z"
     1.5  apply (rule_tac z = z in eq_Abs_hypreal)
     1.6  apply (rule_tac z = w in eq_Abs_hypreal)
     1.7 -apply (simp add: real_add_ac hypreal_add)
     1.8 +apply (simp add: add_ac hypreal_add)
     1.9  done
    1.10  
    1.11  lemma hypreal_add_assoc: "((z1::hypreal) + z2) + z3 = z1 + (z2 + z3)"
    1.12 @@ -419,7 +419,7 @@
    1.13  apply (rule_tac z = z1 in eq_Abs_hypreal)
    1.14  apply (rule_tac z = z2 in eq_Abs_hypreal)
    1.15  apply (rule_tac z = w in eq_Abs_hypreal)
    1.16 -apply (simp add: hypreal_mult hypreal_add real_add_mult_distrib)
    1.17 +apply (simp add: hypreal_mult hypreal_add left_distrib)
    1.18  done
    1.19  
    1.20  text{*one and zero are distinct*}
    1.21 @@ -452,7 +452,7 @@
    1.22  apply (rule_tac z = x in eq_Abs_hypreal)
    1.23  apply (simp add: hypreal_inverse hypreal_mult)
    1.24  apply (drule FreeUltrafilterNat_Compl_mem)
    1.25 -apply (blast intro!: real_mult_inv_right FreeUltrafilterNat_subset)
    1.26 +apply (blast intro!: right_inverse FreeUltrafilterNat_subset)
    1.27  done
    1.28  
    1.29  lemma hypreal_mult_inverse_left:
    1.30 @@ -476,10 +476,6 @@
    1.31    show "y \<noteq> 0 ==> x / y = x * inverse y" by (simp add: hypreal_divide_def)
    1.32  qed
    1.33  
    1.34 -(*Pull negations out*)
    1.35 -declare minus_mult_right [symmetric, simp] 
    1.36 -        minus_mult_left [symmetric, simp]
    1.37 -
    1.38  
    1.39  lemma HYPREAL_INVERSE_ZERO: "inverse 0 = (0::hypreal)"
    1.40  by (simp add: hypreal_inverse hypreal_zero_def)