src/HOL/Real/RealDef.thy
 changeset 14335 9c0b5e081037 parent 14334 6137d24eef79 child 14341 a09441bd4f1e
```--- a/src/HOL/Real/RealDef.thy	Thu Jan 01 10:06:32 2004 +0100
+++ b/src/HOL/Real/RealDef.thy	Thu Jan 01 21:47:07 2004 +0100
@@ -7,26 +7,6 @@

theory RealDef = PReal:

-(*MOVE TO THEORY PREAL*)
-instance preal :: order
-proof qed
- (assumption |
-  rule preal_le_refl preal_le_trans preal_le_anti_sym preal_less_le)+
-
-instance preal :: order
-  by (intro_classes,
-      (assumption |
-       rule preal_le_refl preal_le_trans preal_le_anti_sym preal_less_le)+)
-
-lemma preal_le_linear: "x <= y | y <= (x::preal)"
-apply (insert preal_linear [of x y])
-done
-
-instance preal :: linorder
-  by (intro_classes, rule preal_le_linear)
-
-
constdefs
realrel   ::  "((preal * preal) * (preal * preal)) set"
"realrel == {p. \<exists>x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1}"
@@ -781,8 +761,8 @@

lemma real_of_preal_le_iff:
"(real_of_preal m1 \<le> real_of_preal m2) = (m1 \<le> m2)"
-apply (auto intro!: preal_leI simp add: linorder_not_less [symmetric])
-done
+by (auto intro!: preal_le_iff_less_or_eq [THEN iffD1]

@@ -797,11 +777,15 @@
lemma real_less_add_positive_left_Ex: "R < S ==> \<exists>T::real. 0 < T & R + T = S"
apply (rule_tac x = R in real_of_preal_trichotomyE)
apply (rule_tac [!] x = S in real_of_preal_trichotomyE)