src/HOL/Hyperreal/HyperDef.thy
changeset 14430 5cb24165a2e1
parent 14421 ee97b6463cb4
child 14468 6be497cacab5
     1.1 --- a/src/HOL/Hyperreal/HyperDef.thy	Thu Mar 04 10:06:13 2004 +0100
     1.2 +++ b/src/HOL/Hyperreal/HyperDef.thy	Thu Mar 04 12:06:07 2004 +0100
     1.3 @@ -476,17 +476,14 @@
     1.4    show "(x + y) * z = x * z + y * z" by (simp add: hypreal_add_mult_distrib)
     1.5    show "0 \<noteq> (1::hypreal)" by (rule hypreal_zero_not_eq_one)
     1.6    show "x \<noteq> 0 ==> inverse x * x = 1" by (simp add: hypreal_mult_inverse_left)
     1.7 -  show "y \<noteq> 0 ==> x / y = x * inverse y" by (simp add: hypreal_divide_def)
     1.8 +  show "x / y = x * inverse y" by (simp add: hypreal_divide_def)
     1.9  qed
    1.10  
    1.11  
    1.12  instance hypreal :: division_by_zero
    1.13  proof
    1.14 -  fix x :: hypreal
    1.15 -  show inv: "inverse 0 = (0::hypreal)" 
    1.16 +  show "inverse 0 = (0::hypreal)" 
    1.17      by (simp add: hypreal_inverse hypreal_zero_def)
    1.18 -  show "x/0 = 0" 
    1.19 -    by (simp add: hypreal_divide_def inv hypreal_mult_commute [of a])
    1.20  qed
    1.21  
    1.22