src/HOL/Hyperreal/HyperDef.thy
changeset 14341 a09441bd4f1e
parent 14334 6137d24eef79
child 14348 744c868ee0b7
     1.1 --- a/src/HOL/Hyperreal/HyperDef.thy	Tue Jan 06 10:38:14 2004 +0100
     1.2 +++ b/src/HOL/Hyperreal/HyperDef.thy	Tue Jan 06 10:40:15 2004 +0100
     1.3 @@ -474,6 +474,9 @@
     1.4    show "0 \<noteq> (1::hypreal)" by (rule hypreal_zero_not_eq_one)
     1.5    show "x \<noteq> 0 ==> inverse x * x = 1" by (simp add: hypreal_mult_inverse_left)
     1.6    show "y \<noteq> 0 ==> x / y = x * inverse y" by (simp add: hypreal_divide_def)
     1.7 +  assume eq: "z+x = z+y" 
     1.8 +    hence "(-z + z) + x = (-z + z) + y" by (simp only: eq hypreal_add_assoc)
     1.9 +    thus "x = y" by (simp add: hypreal_add_minus_left)
    1.10  qed
    1.11  
    1.12