diff -r 4e72cd222e0b -r ee97b6463cb4 src/HOL/Hyperreal/HyperDef.thy
--- a/src/HOL/Hyperreal/HyperDef.thy	Mon Mar 01 11:52:59 2004 +0100
+++ b/src/HOL/Hyperreal/HyperDef.thy	Mon Mar 01 13:51:21 2004 +0100
@@ -477,24 +477,16 @@
   show "0 \<noteq> (1::hypreal)" by (rule hypreal_zero_not_eq_one)
   show "x \<noteq> 0 ==> inverse x * x = 1" by (simp add: hypreal_mult_inverse_left)
   show "y \<noteq> 0 ==> x / y = x * inverse y" by (simp add: hypreal_divide_def)
-  assume eq: "z+x = z+y" 
-    hence "(-z + z) + x = (-z + z) + y" by (simp only: eq hypreal_add_assoc)
-    thus "x = y" by (simp add: hypreal_add_minus_left)
 qed
 
 
-lemma HYPREAL_INVERSE_ZERO: "inverse 0 = (0::hypreal)"
-by (simp add: hypreal_inverse hypreal_zero_def)
-
-lemma HYPREAL_DIVISION_BY_ZERO: "a / (0::hypreal) = 0"
-by (simp add: hypreal_divide_def HYPREAL_INVERSE_ZERO 
-              hypreal_mult_commute [of a])
-
 instance hypreal :: division_by_zero
 proof
   fix x :: hypreal
-  show "inverse 0 = (0::hypreal)" by (rule HYPREAL_INVERSE_ZERO)
-  show "x/0 = 0" by (rule HYPREAL_DIVISION_BY_ZERO) 
+  show inv: "inverse 0 = (0::hypreal)" 
+    by (simp add: hypreal_inverse hypreal_zero_def)
+  show "x/0 = 0" 
+    by (simp add: hypreal_divide_def inv hypreal_mult_commute [of a])
 qed
 
 
@@ -569,9 +561,6 @@
 instance hypreal :: ordered_field
 proof
   fix x y z :: hypreal
-  show "0 < (1::hypreal)" 
-    by (simp add: hypreal_zero_def hypreal_one_def linorder_not_le [symmetric],
-        simp add: hypreal_le)
   show "x \<le> y ==> z + x \<le> z + y" 
     by (rule hypreal_add_left_mono)
   show "x < y ==> 0 < z ==> z * x < z * y"