src/HOL/Real/RealDef.thy
 changeset 14421 ee97b6463cb4 parent 14398 c5c47703f763 child 14426 de890c247b38
```--- a/src/HOL/Real/RealDef.thy	Mon Mar 01 11:52:59 2004 +0100
+++ b/src/HOL/Real/RealDef.thy	Mon Mar 01 13:51:21 2004 +0100
@@ -352,9 +352,6 @@
show "0 \<noteq> (1::real)" by (rule real_zero_not_eq_one)
show "x \<noteq> 0 ==> inverse x * x = 1" by (rule real_mult_inverse_left)
show "y \<noteq> 0 ==> x / y = x * inverse y" by (simp add: real_divide_def)
-  assume eq: "z+x = z+y"
-    hence "(-z + z) + x = (-z + z) + y" by (simp only: eq real_add_assoc)
qed

@@ -366,14 +363,11 @@
done

-lemma DIVISION_BY_ZERO: "a / (0::real) = 0"
-  by (simp add: real_divide_def INVERSE_ZERO)
-
instance real :: division_by_zero
proof
fix x :: real
show "inverse 0 = (0::real)" by (rule INVERSE_ZERO)
-  show "x/0 = 0" by (rule DIVISION_BY_ZERO)
+  show "x/0 = 0" by (simp add: real_divide_def INVERSE_ZERO)
qed

@@ -524,8 +518,6 @@
instance real :: ordered_field
proof
fix x y z :: real
-  show "0 < (1::real)"
-    by (simp add: real_less_def real_zero_le_one real_zero_not_eq_one)
show "x \<le> y ==> z + x \<le> z + y" by (rule real_add_left_mono)
show "x < y ==> 0 < z ==> z * x < z * y" by (simp add: real_mult_less_mono2)
show "\<bar>x\<bar> = (if x < 0 then -x else x)"```