# HG changeset patch
# User paulson
# Date 978210798 -3600
# Node ID c4f1bf2acf4ccdcbaabf0b45025c41c8c7ec458c
# Parent  a81ea5d3dd414213b56829e67e65e6378110dd33
tidying, and separation of HOL-Hyperreal from HOL-Real

diff -r a81ea5d3dd41 -r c4f1bf2acf4c src/HOL/Real/HahnBanach/Aux.thy
--- a/src/HOL/Real/HahnBanach/Aux.thy	Sat Dec 30 22:03:47 2000 +0100
+++ b/src/HOL/Real/HahnBanach/Aux.thy	Sat Dec 30 22:13:18 2000 +0100
@@ -17,40 +17,40 @@
 
 text {* \medskip Lemmas about sets. *}
 
-lemma Int_singletonD: "A \<inter> B = {v} \<Longrightarrow> x \<in> A \<Longrightarrow> x \<in> B \<Longrightarrow> x = v"
+lemma Int_singletonD: "A \\<inter> B = {v} \\<Longrightarrow> x \\<in> A \\<Longrightarrow> x \\<in> B \\<Longrightarrow> x = v"
   by (fast elim: equalityE)
 
-lemma set_less_imp_diff_not_empty: "H < E \<Longrightarrow> \<exists>x0 \<in> E. x0 \<notin> H"
+lemma set_less_imp_diff_not_empty: "H < E \\<Longrightarrow> \\<exists>x0 \\<in> E. x0 \\<notin> H"
   by (auto simp add: psubset_eq)
 
 
 text{* \medskip Some lemmas about orders. *}
 
-lemma lt_imp_not_eq: "x < (y::'a::order) \<Longrightarrow> x \<noteq> y"
+lemma lt_imp_not_eq: "x < (y::'a::order) \\<Longrightarrow> x \\<noteq> y"
   by (simp add: order_less_le)
 
 lemma le_noteq_imp_less:
-  "x \<le> (r::'a::order) \<Longrightarrow> x \<noteq> r \<Longrightarrow> x < r"
+  "x \\<le> (r::'a::order) \\<Longrightarrow> x \\<noteq> r \\<Longrightarrow> x < r"
 proof -
-  assume "x \<le> r" and ne:"x \<noteq> r"
-  hence "x < r \<or> x = r" by (simp add: order_le_less)
+  assume "x \\<le> r" and ne:"x \\<noteq> r"
+  hence "x < r \\<or> x = r" by (simp add: order_le_less)
   with ne show ?thesis by simp
 qed
 
 
 text {* \medskip Some lemmas for the reals. *}
 
-lemma real_add_minus_eq: "x - y = (#0::real) \<Longrightarrow> x = y"
+lemma real_add_minus_eq: "x - y = (#0::real) \\<Longrightarrow> x = y"
   by simp
 
 lemma abs_minus_one: "abs (- (#1::real)) = #1"
   by simp
 
 lemma real_mult_le_le_mono1a:
-  "(#0::real) \<le> z \<Longrightarrow> x \<le> y \<Longrightarrow> z * x  \<le> z * y"
+  "(#0::real) \\<le> z \\<Longrightarrow> x \\<le> y \\<Longrightarrow> z * x  \\<le> z * y"
 proof -
-  assume z: "(#0::real) \<le> z" and "x \<le> y"
-  hence "x < y \<or> x = y" by (auto simp add: order_le_less)
+  assume z: "(#0::real) \\<le> z" and "x \\<le> y"
+  hence "x < y \\<or> x = y" by (auto simp add: order_le_less)
   thus ?thesis
   proof
     assume "x < y" show ?thesis by  (rule real_mult_le_less_mono2) simp
@@ -60,10 +60,10 @@
 qed
 
 lemma real_mult_le_le_mono2:
-  "(#0::real) \<le> z \<Longrightarrow> x \<le> y \<Longrightarrow> x * z \<le> y * z"
+  "(#0::real) \\<le> z \\<Longrightarrow> x \\<le> y \\<Longrightarrow> x * z \\<le> y * z"
 proof -
-  assume "(#0::real) \<le> z"  "x \<le> y"
-  hence "x < y \<or> x = y" by (auto simp add: order_le_less)
+  assume "(#0::real) \\<le> z"  "x \\<le> y"
+  hence "x < y \\<or> x = y" by (auto simp add: order_le_less)
   thus ?thesis
   proof
     assume "x < y"
@@ -75,29 +75,29 @@
 qed
 
 lemma real_mult_less_le_anti:
-  "z < (#0::real) \<Longrightarrow> x \<le> y \<Longrightarrow> z * y \<le> z * x"
+  "z < (#0::real) \\<Longrightarrow> x \\<le> y \\<Longrightarrow> z * y \\<le> z * x"
 proof -
-  assume "z < #0"  "x \<le> y"
+  assume "z < #0"  "x \\<le> y"
   hence "#0 < - z" by simp
-  hence "#0 \<le> - z" by (rule real_less_imp_le)
-  hence "x * (- z) \<le> y * (- z)"
+  hence "#0 \\<le> - z" by (rule order_less_imp_le)
+  hence "x * (- z) \\<le> y * (- z)"
     by (rule real_mult_le_le_mono2)
-  hence  "- (x * z) \<le> - (y * z)"
+  hence  "- (x * z) \\<le> - (y * z)"
     by (simp only: real_minus_mult_eq2)
   thus ?thesis by (simp only: real_mult_commute)
 qed
 
 lemma real_mult_less_le_mono:
-  "(#0::real) < z \<Longrightarrow> x \<le> y \<Longrightarrow> z * x \<le> z * y"
+  "(#0::real) < z \\<Longrightarrow> x \\<le> y \\<Longrightarrow> z * x \\<le> z * y"
 proof -
-  assume "#0 < z"  "x \<le> y"
-  have "#0 \<le> z" by (rule real_less_imp_le)
-  hence "x * z \<le> y * z"
+  assume "#0 < z"  "x \\<le> y"
+  have "#0 \\<le> z" by (rule order_less_imp_le)
+  hence "x * z \\<le> y * z"
     by (rule real_mult_le_le_mono2)
   thus ?thesis by (simp only: real_mult_commute)
 qed
 
-lemma real_inverse_gt_zero1: "#0 < (x::real) \<Longrightarrow> #0 < inverse x"
+lemma real_inverse_gt_zero1: "#0 < (x::real) \\<Longrightarrow> #0 < inverse x"
 proof -
   assume "#0 < x"
   have "0 < x" by simp
@@ -105,17 +105,17 @@
   thus ?thesis by simp
 qed
 
-lemma real_mult_inv_right1: "(x::real) \<noteq> #0 \<Longrightarrow> x * inverse x = #1"
+lemma real_mult_inv_right1: "(x::real) \\<noteq> #0 \\<Longrightarrow> x * inverse x = #1"
   by simp
 
-lemma real_mult_inv_left1: "(x::real) \<noteq> #0 \<Longrightarrow> inverse x * x = #1"
+lemma real_mult_inv_left1: "(x::real) \\<noteq> #0 \\<Longrightarrow> inverse x * x = #1"
   by simp
 
 lemma real_le_mult_order1a:
-  "(#0::real) \<le> x \<Longrightarrow> #0 \<le> y \<Longrightarrow> #0 \<le> x * y"
+  "(#0::real) \\<le> x \\<Longrightarrow> #0 \\<le> y \\<Longrightarrow> #0 \\<le> x * y"
 proof -
-  assume "#0 \<le> x"  "#0 \<le> y"
-  have "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> 0 \<le> x * y"
+  assume "#0 \\<le> x"  "#0 \\<le> y"
+  have "0 \\<le> x \\<Longrightarrow> 0 \\<le> y \\<Longrightarrow> 0 \\<le> x * y"
     by (rule real_le_mult_order)
   thus ?thesis by (simp!)
 qed
@@ -141,11 +141,11 @@
   finally show ?thesis .
 qed
 
-lemma real_minus_le: "- (x::real) \<le> y \<Longrightarrow> - y \<le> x"
+lemma real_minus_le: "- (x::real) \\<le> y \\<Longrightarrow> - y \\<le> x"
   by simp
 
 lemma real_diff_ineq_swap:
-    "(d::real) - b \<le> c + a \<Longrightarrow> - a - b \<le> c - d"
+    "(d::real) - b \\<le> c + a \\<Longrightarrow> - a - b \\<le> c - d"
   by simp
 
 end
diff -r a81ea5d3dd41 -r c4f1bf2acf4c src/HOL/Real/HahnBanach/FunctionNorm.thy
--- a/src/HOL/Real/HahnBanach/FunctionNorm.thy	Sat Dec 30 22:03:47 2000 +0100
+++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy	Sat Dec 30 22:13:18 2000 +0100
@@ -10,10 +10,10 @@
 subsection {* Continuous linear forms*}
 
 text {*
-  A linear form @{text f} on a normed vector space @{text "(V, \<parallel>\<cdot>\<parallel>)"}
+  A linear form @{text f} on a normed vector space @{text "(V, \\<parallel>\\<cdot>\\<parallel>)"}
   is \emph{continuous}, iff it is bounded, i.~e.
   \begin{center}
-  @{text "\<exists>c \<in> R. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"}
+  @{text "\\<exists>c \\<in> R. \\<forall>x \\<in> V. \\<bar>f x\\<bar> \\<le> c \\<cdot> \\<parallel>x\\<parallel>"}
   \end{center}
   In our application no other functions than linear forms are
   considered, so we can define continuous linear forms as bounded
@@ -22,25 +22,25 @@
 
 constdefs
   is_continuous ::
-  "'a::{plus, minus, zero} set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> bool"
-  "is_continuous V norm f \<equiv>
-    is_linearform V f \<and> (\<exists>c. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c * norm x)"
+  "'a::{plus, minus, zero} set \\<Rightarrow> ('a \\<Rightarrow> real) \\<Rightarrow> ('a \\<Rightarrow> real) \\<Rightarrow> bool"
+  "is_continuous V norm f \\<equiv>
+    is_linearform V f \\<and> (\\<exists>c. \\<forall>x \\<in> V. \\<bar>f x\\<bar> \\<le> c * norm x)"
 
 lemma continuousI [intro]:
-  "is_linearform V f \<Longrightarrow> (\<And>x. x \<in> V \<Longrightarrow> \<bar>f x\<bar> \<le> c * norm x)
-  \<Longrightarrow> is_continuous V norm f"
+  "is_linearform V f \\<Longrightarrow> (\\<And>x. x \\<in> V \\<Longrightarrow> \\<bar>f x\\<bar> \\<le> c * norm x)
+  \\<Longrightarrow> is_continuous V norm f"
 proof (unfold is_continuous_def, intro exI conjI ballI)
-  assume r: "\<And>x. x \<in> V \<Longrightarrow> \<bar>f x\<bar> \<le> c * norm x"
-  fix x assume "x \<in> V" show "\<bar>f x\<bar> \<le> c * norm x" by (rule r)
+  assume r: "\\<And>x. x \\<in> V \\<Longrightarrow> \\<bar>f x\\<bar> \\<le> c * norm x"
+  fix x assume "x \\<in> V" show "\\<bar>f x\\<bar> \\<le> c * norm x" by (rule r)
 qed
 
 lemma continuous_linearform [intro?]:
-  "is_continuous V norm f \<Longrightarrow> is_linearform V f"
+  "is_continuous V norm f \\<Longrightarrow> is_linearform V f"
   by (unfold is_continuous_def) blast
 
 lemma continuous_bounded [intro?]:
   "is_continuous V norm f
-  \<Longrightarrow> \<exists>c. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c * norm x"
+  \\<Longrightarrow> \\<exists>c. \\<forall>x \\<in> V. \\<bar>f x\\<bar> \\<le> c * norm x"
   by (unfold is_continuous_def) blast
 
 subsection{* The norm of a linear form *}
@@ -49,34 +49,34 @@
 text {*
   The least real number @{text c} for which holds
   \begin{center}
-  @{text "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"}
+  @{text "\\<forall>x \\<in> V. \\<bar>f x\\<bar> \\<le> c \\<cdot> \\<parallel>x\\<parallel>"}
   \end{center}
   is called the \emph{norm} of @{text f}.
 
-  For non-trivial vector spaces @{text "V \<noteq> {0}"} the norm can be
+  For non-trivial vector spaces @{text "V \\<noteq> {0}"} the norm can be
   defined as
   \begin{center}
-  @{text "\<parallel>f\<parallel> = \<sup>x \<noteq> 0. \<bar>f x\<bar> / \<parallel>x\<parallel>"}
+  @{text "\\<parallel>f\\<parallel> = \<sup>x \\<noteq> 0. \\<bar>f x\\<bar> / \\<parallel>x\\<parallel>"}
   \end{center}
 
   For the case @{text "V = {0}"} the supremum would be taken from an
-  empty set. Since @{text \<real>} is unbounded, there would be no supremum.
+  empty set. Since @{text \\<real>} is unbounded, there would be no supremum.
   To avoid this situation it must be guaranteed that there is an
-  element in this set. This element must be @{text "{} \<ge> 0"} so that
+  element in this set. This element must be @{text "{} \\<ge> 0"} so that
   @{text function_norm} has the norm properties. Furthermore
   it does not have to change the norm in all other cases, so it must
-  be @{text 0}, as all other elements of are @{text "{} \<ge> 0"}.
+  be @{text 0}, as all other elements of are @{text "{} \\<ge> 0"}.
 
   Thus we define the set @{text B} the supremum is taken from as
   \begin{center}
-  @{text "{0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel>. x \<noteq> 0 \<and> x \<in> F}"}
+  @{text "{0} \\<union> {\\<bar>f x\\<bar> / \\<parallel>x\\<parallel>. x \\<noteq> 0 \\<and> x \\<in> F}"}
   \end{center}
 *}
 
 constdefs
-  B :: "'a set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> ('a::{plus, minus, zero} \<Rightarrow> real) \<Rightarrow> real set"
-  "B V norm f \<equiv>
-  {#0} \<union> {\<bar>f x\<bar> * inverse (norm x) | x. x \<noteq> 0 \<and> x \<in> V}"
+  B :: "'a set \\<Rightarrow> ('a \\<Rightarrow> real) \\<Rightarrow> ('a::{plus, minus, zero} \\<Rightarrow> real) \\<Rightarrow> real set"
+  "B V norm f \\<equiv>
+  {#0} \\<union> {\\<bar>f x\\<bar> * inverse (norm x) | x. x \\<noteq> 0 \\<and> x \\<in> V}"
 
 text {*
   @{text n} is the function norm of @{text f}, iff @{text n} is the
@@ -85,8 +85,8 @@
 
 constdefs
   is_function_norm ::
-  "('a::{minus,plus,zero} \<Rightarrow> real) \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> real \<Rightarrow> bool"
-  "is_function_norm f V norm fn \<equiv> is_Sup UNIV (B V norm f) fn"
+  "('a::{minus,plus,zero} \\<Rightarrow> real) \\<Rightarrow> 'a set \\<Rightarrow> ('a \\<Rightarrow> real) \\<Rightarrow> real \\<Rightarrow> bool"
+  "is_function_norm f V norm fn \\<equiv> is_Sup UNIV (B V norm f) fn"
 
 text {*
   @{text function_norm} is equal to the supremum of @{text B}, if the
@@ -94,159 +94,159 @@
 *}
 
 constdefs
-  function_norm :: "('a::{minus,plus,zero} \<Rightarrow> real) \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> real"
-  "function_norm f V norm \<equiv> Sup UNIV (B V norm f)"
+  function_norm :: "('a::{minus,plus,zero} \\<Rightarrow> real) \\<Rightarrow> 'a set \\<Rightarrow> ('a \\<Rightarrow> real) \\<Rightarrow> real"
+  "function_norm f V norm \\<equiv> Sup UNIV (B V norm f)"
 
 syntax
-  function_norm :: "('a \<Rightarrow> real) \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> real"  ("\<parallel>_\<parallel>_,_")
+  function_norm :: "('a \\<Rightarrow> real) \\<Rightarrow> 'a set \\<Rightarrow> ('a \\<Rightarrow> real) \\<Rightarrow> real"  ("\\<parallel>_\\<parallel>_,_")
 
-lemma B_not_empty: "#0 \<in> B V norm f"
+lemma B_not_empty: "#0 \\<in> B V norm f"
   by (unfold B_def) blast
 
 text {*
   The following lemma states that every continuous linear form on a
-  normed space @{text "(V, \<parallel>\<cdot>\<parallel>)"} has a function norm.
+  normed space @{text "(V, \\<parallel>\\<cdot>\\<parallel>)"} has a function norm.
 *}
 
 lemma ex_fnorm [intro?]:
-  "is_normed_vectorspace V norm \<Longrightarrow> is_continuous V norm f
-     \<Longrightarrow> is_function_norm f V norm \<parallel>f\<parallel>V,norm"
+  "is_normed_vectorspace V norm \\<Longrightarrow> is_continuous V norm f
+     \\<Longrightarrow> is_function_norm f V norm \\<parallel>f\\<parallel>V,norm"
 proof (unfold function_norm_def is_function_norm_def
   is_continuous_def Sup_def, elim conjE, rule someI2_ex)
   assume "is_normed_vectorspace V norm"
   assume "is_linearform V f"
-  and e: "\<exists>c. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c * norm x"
+  and e: "\\<exists>c. \\<forall>x \\<in> V. \\<bar>f x\\<bar> \\<le> c * norm x"
 
   txt {* The existence of the supremum is shown using the
   completeness of the reals. Completeness means, that
   every non-empty bounded set of reals has a
   supremum. *}
-  show  "\<exists>a. is_Sup UNIV (B V norm f) a"
+  show  "\\<exists>a. is_Sup UNIV (B V norm f) a"
   proof (unfold is_Sup_def, rule reals_complete)
 
     txt {* First we have to show that @{text B} is non-empty: *}
 
-    show "\<exists>X. X \<in> B V norm f"
+    show "\\<exists>X. X \\<in> B V norm f"
     proof
-      show "#0 \<in> (B V norm f)" by (unfold B_def) blast
+      show "#0 \\<in> (B V norm f)" by (unfold B_def) blast
     qed
 
     txt {* Then we have to show that @{text B} is bounded: *}
 
-    from e show "\<exists>Y. isUb UNIV (B V norm f) Y"
+    from e show "\\<exists>Y. isUb UNIV (B V norm f) Y"
     proof
 
       txt {* We know that @{text f} is bounded by some value @{text c}. *}
 
-      fix c assume a: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * norm x"
-      def b \<equiv> "max c #0"
+      fix c assume a: "\\<forall>x \\<in> V. \\<bar>f x\\<bar> \\<le> c * norm x"
+      def b \\<equiv> "max c #0"
 
       show "?thesis"
       proof (intro exI isUbI setleI ballI, unfold B_def,
         elim UnE CollectE exE conjE singletonE)
 
         txt {* To proof the thesis, we have to show that there is some
-        constant @{text b}, such that @{text "y \<le> b"} for all
-        @{text "y \<in> B"}. Due to the definition of @{text B} there are
-        two cases for @{text "y \<in> B"}.  If @{text "y = 0"} then
-        @{text "y \<le> max c 0"}: *}
+        constant @{text b}, such that @{text "y \\<le> b"} for all
+        @{text "y \\<in> B"}. Due to the definition of @{text B} there are
+        two cases for @{text "y \\<in> B"}.  If @{text "y = 0"} then
+        @{text "y \\<le> max c 0"}: *}
 
         fix y assume "y = (#0::real)"
-        show "y \<le> b" by (simp! add: le_maxI2)
+        show "y \\<le> b" by (simp! add: le_maxI2)
 
-        txt {* The second case is @{text "y = \<bar>f x\<bar> / \<parallel>x\<parallel>"} for some
-        @{text "x \<in> V"} with @{text "x \<noteq> 0"}. *}
+        txt {* The second case is @{text "y = \\<bar>f x\\<bar> / \\<parallel>x\\<parallel>"} for some
+        @{text "x \\<in> V"} with @{text "x \\<noteq> 0"}. *}
 
       next
         fix x y
-        assume "x \<in> V"  "x \<noteq> 0"
+        assume "x \\<in> V"  "x \\<noteq> 0"
 
         txt {* The thesis follows by a short calculation using the
         fact that @{text f} is bounded. *}
 
-        assume "y = \<bar>f x\<bar> * inverse (norm x)"
-        also have "... \<le> c * norm x * inverse (norm x)"
+        assume "y = \\<bar>f x\\<bar> * inverse (norm x)"
+        also have "... \\<le> c * norm x * inverse (norm x)"
         proof (rule real_mult_le_le_mono2)
-          show "#0 \<le> inverse (norm x)"
-            by (rule real_less_imp_le, rule real_inverse_gt_zero1,
+          show "#0 \\<le> inverse (norm x)"
+            by (rule order_less_imp_le, rule real_inverse_gt_zero1,
                 rule normed_vs_norm_gt_zero)
-          from a show "\<bar>f x\<bar> \<le> c * norm x" ..
+          from a show "\\<bar>f x\\<bar> \\<le> c * norm x" ..
         qed
         also have "... = c * (norm x * inverse (norm x))"
           by (rule real_mult_assoc)
         also have "(norm x * inverse (norm x)) = (#1::real)"
         proof (rule real_mult_inv_right1)
-          show nz: "norm x \<noteq> #0"
+          show nz: "norm x \\<noteq> #0"
             by (rule not_sym, rule lt_imp_not_eq,
               rule normed_vs_norm_gt_zero)
         qed
-        also have "c * ... \<le> b " by (simp! add: le_maxI1)
-        finally show "y \<le> b" .
+        also have "c * ... \\<le> b " by (simp! add: le_maxI1)
+        finally show "y \\<le> b" .
       qed simp
     qed
   qed
 qed
 
-text {* The norm of a continuous function is always @{text "\<ge> 0"}. *}
+text {* The norm of a continuous function is always @{text "\\<ge> 0"}. *}
 
 lemma fnorm_ge_zero [intro?]:
-  "is_continuous V norm f \<Longrightarrow> is_normed_vectorspace V norm
-   \<Longrightarrow> #0 \<le> \<parallel>f\<parallel>V,norm"
+  "is_continuous V norm f \\<Longrightarrow> is_normed_vectorspace V norm
+   \\<Longrightarrow> #0 \\<le> \\<parallel>f\\<parallel>V,norm"
 proof -
   assume c: "is_continuous V norm f"
      and n: "is_normed_vectorspace V norm"
 
   txt {* The function norm is defined as the supremum of @{text B}.
-  So it is @{text "\<ge> 0"} if all elements in @{text B} are
-  @{text "\<ge> 0"}, provided the supremum exists and @{text B} is not
+  So it is @{text "\\<ge> 0"} if all elements in @{text B} are
+  @{text "\\<ge> 0"}, provided the supremum exists and @{text B} is not
   empty. *}
 
   show ?thesis
   proof (unfold function_norm_def, rule sup_ub1)
-    show "\<forall>x \<in> (B V norm f). #0 \<le> x"
+    show "\\<forall>x \\<in> (B V norm f). #0 \\<le> x"
     proof (intro ballI, unfold B_def,
            elim UnE singletonE CollectE exE conjE)
       fix x r
-      assume "x \<in> V"  "x \<noteq> 0"
-        and r: "r = \<bar>f x\<bar> * inverse (norm x)"
+      assume "x \\<in> V"  "x \\<noteq> 0"
+        and r: "r = \\<bar>f x\\<bar> * inverse (norm x)"
 
-      have ge: "#0 \<le> \<bar>f x\<bar>" by (simp! only: abs_ge_zero)
-      have "#0 \<le> inverse (norm x)"
-        by (rule real_less_imp_le, rule real_inverse_gt_zero1, rule)(***
-        proof (rule real_less_imp_le);
+      have ge: "#0 \\<le> \\<bar>f x\\<bar>" by (simp! only: abs_ge_zero)
+      have "#0 \\<le> inverse (norm x)"
+        by (rule order_less_imp_le, rule real_inverse_gt_zero1, rule)(***
+        proof (rule order_less_imp_le);
           show "#0 < inverse (norm x)";
           proof (rule real_inverse_gt_zero);
             show "#0 < norm x"; ..;
           qed;
         qed; ***)
-      with ge show "#0 \<le> r"
+      with ge show "#0 \\<le> r"
        by (simp only: r, rule real_le_mult_order1a)
     qed (simp!)
 
     txt {* Since @{text f} is continuous the function norm exists: *}
 
-    have "is_function_norm f V norm \<parallel>f\<parallel>V,norm" ..
+    have "is_function_norm f V norm \\<parallel>f\\<parallel>V,norm" ..
     thus "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))"
       by (unfold is_function_norm_def function_norm_def)
 
     txt {* @{text B} is non-empty by construction: *}
 
-    show "#0 \<in> B V norm f" by (rule B_not_empty)
+    show "#0 \\<in> B V norm f" by (rule B_not_empty)
   qed
 qed
 
 text {*
   \medskip The fundamental property of function norms is:
   \begin{center}
-  @{text "\<bar>f x\<bar> \<le> \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>"}
+  @{text "\\<bar>f x\\<bar> \\<le> \\<parallel>f\\<parallel> \\<cdot> \\<parallel>x\\<parallel>"}
   \end{center}
 *}
 
 lemma norm_fx_le_norm_f_norm_x:
-  "is_continuous V norm f \<Longrightarrow> is_normed_vectorspace V norm \<Longrightarrow> x \<in> V
-    \<Longrightarrow> \<bar>f x\<bar> \<le> \<parallel>f\<parallel>V,norm * norm x"
+  "is_continuous V norm f \\<Longrightarrow> is_normed_vectorspace V norm \\<Longrightarrow> x \\<in> V
+    \\<Longrightarrow> \\<bar>f x\\<bar> \\<le> \\<parallel>f\\<parallel>V,norm * norm x"
 proof -
-  assume "is_normed_vectorspace V norm"  "x \<in> V"
+  assume "is_normed_vectorspace V norm"  "x \\<in> V"
   and c: "is_continuous V norm f"
   have v: "is_vectorspace V" ..
 
@@ -260,46 +260,46 @@
     @{text "f 0 = 0"}. *}
 
     assume "x = 0"
-    have "\<bar>f x\<bar> = \<bar>f 0\<bar>" by (simp!)
+    have "\\<bar>f x\\<bar> = \\<bar>f 0\\<bar>" by (simp!)
     also from v continuous_linearform have "f 0 = #0" ..
     also note abs_zero
-    also have "#0 \<le> \<parallel>f\<parallel>V,norm * norm x"
+    also have "#0 \\<le> \\<parallel>f\\<parallel>V,norm * norm x"
     proof (rule real_le_mult_order1a)
-      show "#0 \<le> \<parallel>f\<parallel>V,norm" ..
-      show "#0 \<le> norm x" ..
+      show "#0 \\<le> \\<parallel>f\\<parallel>V,norm" ..
+      show "#0 \\<le> norm x" ..
     qed
     finally
-    show "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>V,norm * norm x" .
+    show "\\<bar>f x\\<bar> \\<le> \\<parallel>f\\<parallel>V,norm * norm x" .
 
   next
-    assume "x \<noteq> 0"
+    assume "x \\<noteq> 0"
     have n: "#0 < norm x" ..
-    hence nz: "norm x \<noteq> #0"
+    hence nz: "norm x \\<noteq> #0"
       by (simp only: lt_imp_not_eq)
 
-    txt {* For the case @{text "x \<noteq> 0"} we derive the following fact
+    txt {* For the case @{text "x \\<noteq> 0"} we derive the following fact
     from the definition of the function norm:*}
 
-    have l: "\<bar>f x\<bar> * inverse (norm x) \<le> \<parallel>f\<parallel>V,norm"
+    have l: "\\<bar>f x\\<bar> * inverse (norm x) \\<le> \\<parallel>f\\<parallel>V,norm"
     proof (unfold function_norm_def, rule sup_ub)
       from ex_fnorm [OF _ c]
       show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))"
          by (simp! add: is_function_norm_def function_norm_def)
-      show "\<bar>f x\<bar> * inverse (norm x) \<in> B V norm f"
+      show "\\<bar>f x\\<bar> * inverse (norm x) \\<in> B V norm f"
         by (unfold B_def, intro UnI2 CollectI exI [of _ x]
             conjI, simp)
     qed
 
     txt {* The thesis now follows by a short calculation: *}
 
-    have "\<bar>f x\<bar> = \<bar>f x\<bar> * #1" by (simp!)
+    have "\\<bar>f x\\<bar> = \\<bar>f x\\<bar> * #1" by (simp!)
     also from nz have "#1 = inverse (norm x) * norm x"
       by (simp add: real_mult_inv_left1)
-    also have "\<bar>f x\<bar> * ... = \<bar>f x\<bar> * inverse (norm x) * norm x"
+    also have "\\<bar>f x\\<bar> * ... = \\<bar>f x\\<bar> * inverse (norm x) * norm x"
       by (simp! add: real_mult_assoc)
-    also from n l have "... \<le> \<parallel>f\<parallel>V,norm * norm x"
+    also from n l have "... \\<le> \\<parallel>f\\<parallel>V,norm * norm x"
       by (simp add: real_mult_le_le_mono2)
-    finally show "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>V,norm * norm x" .
+    finally show "\\<bar>f x\\<bar> \\<le> \\<parallel>f\\<parallel>V,norm * norm x" .
   qed
 qed
 
@@ -307,72 +307,72 @@
   \medskip The function norm is the least positive real number for
   which the following inequation holds:
   \begin{center}
-  @{text "\<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"}
+  @{text "\\<bar>f x\\<bar> \\<le> c \\<cdot> \\<parallel>x\\<parallel>"}
   \end{center}
 *}
 
 lemma fnorm_le_ub:
-  "is_continuous V norm f \<Longrightarrow> is_normed_vectorspace V norm \<Longrightarrow>
-     \<forall>x \<in> V. \<bar>f x\<bar> \<le> c * norm x \<Longrightarrow> #0 \<le> c
-  \<Longrightarrow> \<parallel>f\<parallel>V,norm \<le> c"
+  "is_continuous V norm f \\<Longrightarrow> is_normed_vectorspace V norm \\<Longrightarrow>
+     \\<forall>x \\<in> V. \\<bar>f x\\<bar> \\<le> c * norm x \\<Longrightarrow> #0 \\<le> c
+  \\<Longrightarrow> \\<parallel>f\\<parallel>V,norm \\<le> c"
 proof (unfold function_norm_def)
   assume "is_normed_vectorspace V norm"
   assume c: "is_continuous V norm f"
-  assume fb: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * norm x"
-    and "#0 \<le> c"
+  assume fb: "\\<forall>x \\<in> V. \\<bar>f x\\<bar> \\<le> c * norm x"
+    and "#0 \\<le> c"
 
-  txt {* Suppose the inequation holds for some @{text "c \<ge> 0"}.  If
+  txt {* Suppose the inequation holds for some @{text "c \\<ge> 0"}.  If
   @{text c} is an upper bound of @{text B}, then @{text c} is greater
   than the function norm since the function norm is the least upper
   bound.  *}
 
-  show "Sup UNIV (B V norm f) \<le> c"
+  show "Sup UNIV (B V norm f) \\<le> c"
   proof (rule sup_le_ub)
     from ex_fnorm [OF _ c]
     show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))"
       by (simp! add: is_function_norm_def function_norm_def)
 
     txt {* @{text c} is an upper bound of @{text B}, i.e. every
-    @{text "y \<in> B"} is less than @{text c}. *}
+    @{text "y \\<in> B"} is less than @{text c}. *}
 
     show "isUb UNIV (B V norm f) c"
     proof (intro isUbI setleI ballI)
-      fix y assume "y \<in> B V norm f"
-      thus le: "y \<le> c"
+      fix y assume "y \\<in> B V norm f"
+      thus le: "y \\<le> c"
       proof (unfold B_def, elim UnE CollectE exE conjE singletonE)
 
-       txt {* The first case for @{text "y \<in> B"} is @{text "y = 0"}. *}
+       txt {* The first case for @{text "y \\<in> B"} is @{text "y = 0"}. *}
 
         assume "y = #0"
-        show "y \<le> c" by (blast!)
+        show "y \\<le> c" by (blast!)
 
-        txt{* The second case is @{text "y = \<bar>f x\<bar> / \<parallel>x\<parallel>"} for some
-        @{text "x \<in> V"} with @{text "x \<noteq> 0"}. *}
+        txt{* The second case is @{text "y = \\<bar>f x\\<bar> / \\<parallel>x\\<parallel>"} for some
+        @{text "x \\<in> V"} with @{text "x \\<noteq> 0"}. *}
 
       next
         fix x
-        assume "x \<in> V"  "x \<noteq> 0"
+        assume "x \\<in> V"  "x \\<noteq> 0"
 
         have lz: "#0 < norm x"
           by (simp! add: normed_vs_norm_gt_zero)
 
-        have nz: "norm x \<noteq> #0"
+        have nz: "norm x \\<noteq> #0"
         proof (rule not_sym)
-          from lz show "#0 \<noteq> norm x"
+          from lz show "#0 \\<noteq> norm x"
             by (simp! add: order_less_imp_not_eq)
         qed
 
         from lz have "#0 < inverse (norm x)"
           by (simp! add: real_inverse_gt_zero1)
-        hence inverse_gez: "#0 \<le> inverse (norm x)"
-          by (rule real_less_imp_le)
+        hence inverse_gez: "#0 \\<le> inverse (norm x)"
+          by (rule order_less_imp_le)
 
-        assume "y = \<bar>f x\<bar> * inverse (norm x)"
-        also from inverse_gez have "... \<le> c * norm x * inverse (norm x)"
+        assume "y = \\<bar>f x\\<bar> * inverse (norm x)"
+        also from inverse_gez have "... \\<le> c * norm x * inverse (norm x)"
           proof (rule real_mult_le_le_mono2)
-            show "\<bar>f x\<bar> \<le> c * norm x" by (rule bspec)
+            show "\\<bar>f x\\<bar> \\<le> c * norm x" by (rule bspec)
           qed
-        also have "... \<le> c" by (simp add: nz real_mult_assoc)
+        also have "... \\<le> c" by (simp add: nz real_mult_assoc)
         finally show ?thesis .
       qed
     qed blast
diff -r a81ea5d3dd41 -r c4f1bf2acf4c src/HOL/Real/HahnBanach/ROOT.ML
--- a/src/HOL/Real/HahnBanach/ROOT.ML	Sat Dec 30 22:03:47 2000 +0100
+++ b/src/HOL/Real/HahnBanach/ROOT.ML	Sat Dec 30 22:13:18 2000 +0100
@@ -5,4 +5,4 @@
 The Hahn-Banach theorem for real vector spaces (Isabelle/Isar).
 *)
 
-time_use_thy "HahnBanach";
+with_path "../../Hyperreal" time_use_thy "HahnBanach";
diff -r a81ea5d3dd41 -r c4f1bf2acf4c src/HOL/Real/PNat.ML
--- a/src/HOL/Real/PNat.ML	Sat Dec 30 22:03:47 2000 +0100
+++ b/src/HOL/Real/PNat.ML	Sat Dec 30 22:13:18 2000 +0100
@@ -232,18 +232,6 @@
 
   (*** pnat_less ***)
 
-Goalw [pnat_less_def] 
-      "[| x < (y::pnat); y < z |] ==> x < z";
-by ((etac less_trans 1) THEN assume_tac 1);
-qed "pnat_less_trans";
-
-Goalw [pnat_less_def] "x < (y::pnat) ==> ~ y < x";
-by (etac less_not_sym 1);
-qed "pnat_less_not_sym";
-
-(* [| x < y;  ~P ==> y < x |] ==> P *)
-bind_thm ("pnat_less_asym", pnat_less_not_sym RS contrapos_np);
-
 Goalw [pnat_less_def] "~ y < (y::pnat)";
 by Auto_tac;
 qed "pnat_less_not_refl";
@@ -296,77 +284,6 @@
 
    (*** pnat_le ***)
 
-Goalw [pnat_le_def] "~ (x::pnat) < y ==> y <= x";
-by (assume_tac 1);
-qed "pnat_leI";
-
-Goalw [pnat_le_def] "(x::pnat) <= y ==> ~ y < x";
-by (assume_tac 1);
-qed "pnat_leD";
-
-bind_thm ("pnat_leE", make_elim pnat_leD);
-
-Goal "(~ (x::pnat) < y) = (y <= x)";
-by (blast_tac (claset() addIs [pnat_leI] addEs [pnat_leE]) 1);
-qed "pnat_not_less_iff_le";
-
-Goalw [pnat_le_def] "~(x::pnat) <= y ==> y < x";
-by (Blast_tac 1);
-qed "pnat_not_leE";
-
-Goalw [pnat_le_def] "(x::pnat) < y ==> x <= y";
-by (blast_tac (claset() addEs [pnat_less_asym]) 1);
-qed "pnat_less_imp_le";
-
-(** Equivalence of m<=n and  m<n | m=n **)
-
-Goalw [pnat_le_def] "m <= n ==> m < n | m=(n::pnat)";
-by (cut_facts_tac [pnat_less_linear] 1);
-by (blast_tac (claset() addEs [pnat_less_irrefl,pnat_less_asym]) 1);
-qed "pnat_le_imp_less_or_eq";
-
-Goalw [pnat_le_def] "m<n | m=n ==> m <=(n::pnat)";
-by (cut_facts_tac [pnat_less_linear] 1);
-by (blast_tac (claset() addSEs [pnat_less_irrefl] addEs [pnat_less_asym]) 1);
-qed "pnat_less_or_eq_imp_le";
-
-Goal "(m <= (n::pnat)) = (m < n | m=n)";
-by (REPEAT(ares_tac [iffI,pnat_less_or_eq_imp_le,pnat_le_imp_less_or_eq] 1));
-qed "pnat_le_eq_less_or_eq";
-
-Goal "n <= (n::pnat)";
-by (simp_tac (simpset() addsimps [pnat_le_eq_less_or_eq]) 1);
-qed "pnat_le_refl";
-
-Goal "[| i < j; j <= k |] ==> i < (k::pnat)";
-by (dtac pnat_le_imp_less_or_eq 1);
-by (blast_tac (claset() addIs [pnat_less_trans]) 1);
-qed "pnat_less_le_trans";
-
-Goal "[| i <= j; j <= k |] ==> i <= (k::pnat)";
-by (EVERY1[dtac pnat_le_imp_less_or_eq, 
-           dtac pnat_le_imp_less_or_eq,
-           rtac pnat_less_or_eq_imp_le, 
-           blast_tac (claset() addIs [pnat_less_trans])]);
-qed "pnat_le_trans";
-
-Goal "[| m <= n; n <= m |] ==> m = (n::pnat)";
-by (EVERY1[dtac pnat_le_imp_less_or_eq, 
-           dtac pnat_le_imp_less_or_eq,
-           blast_tac (claset() addIs [pnat_less_asym])]);
-qed "pnat_le_anti_sym";
-
-Goal "(m::pnat) < n = (m <= n & m ~= n)";
-by (rtac iffI 1);
-by (rtac conjI 1);
-by (etac pnat_less_imp_le 1);
-by (etac pnat_less_not_refl2 1);
-by (blast_tac (claset() addSDs [pnat_le_imp_less_or_eq]) 1);
-qed "pnat_less_le";
-
-
-(***) (***) (***) (***) (***) (***) (***) (***)
-
 (*** alternative definition for pnat_le ***)
 Goalw [pnat_le_def,pnat_less_def] 
       "((m::pnat) <= n) = (Rep_pnat m <= Rep_pnat n)";
@@ -403,7 +320,7 @@
 
 Goal "m + k <= n --> m <= (n::pnat)";
 by (simp_tac (simpset() addsimps [pnat_le_iff_Rep_pnat_le,
-    sum_Rep_pnat_sum RS sym]) 1);
+                                  sum_Rep_pnat_sum RS sym]) 1);
 qed_spec_mp "pnat_add_leD1";
 
 Goal "!!n::pnat. m + k <= n ==> k <= n";
@@ -448,39 +365,6 @@
 
 (*** Monotonicity of Addition ***)
 
-(*strict, in 1st argument*)
-Goalw [pnat_less_def] "!!i j k::pnat. i < j ==> i + k < j + k";
-by (auto_tac (claset() addIs [add_less_mono1],
-       simpset() addsimps [sum_Rep_pnat_sum RS sym]));
-qed "pnat_add_less_mono1";
-
-Goalw [pnat_less_def] "!!i j k::pnat. [|i < j; k < l|] ==> i + k < j + l";
-by (auto_tac (claset() addIs [add_less_mono],
-       simpset() addsimps [sum_Rep_pnat_sum RS sym]));
-qed "pnat_add_less_mono";
-
-Goalw [pnat_less_def]
-"!!f. [| !!i j::pnat. i<j ==> f(i) < f(j);       \
-\        i <= j                                 \
-\     |] ==> f(i) <= (f(j)::pnat)";
-by (auto_tac (claset() addSDs [inj_Rep_pnat RS injD],
-             simpset() addsimps [pnat_le_iff_Rep_pnat_le,
-				 order_le_less]));
-qed "pnat_less_mono_imp_le_mono";
-
-Goal "!!i j k::pnat. i<=j ==> i + k <= j + k";
-by (res_inst_tac [("f", "%j. j+k")] pnat_less_mono_imp_le_mono 1);
-by (etac pnat_add_less_mono1 1);
-by (assume_tac 1);
-qed "pnat_add_le_mono1";
-
-Goal "!!k l::pnat. [|i<=j;  k<=l |] ==> i + k <= j + l";
-by (etac (pnat_add_le_mono1 RS pnat_le_trans) 1);
-by (simp_tac (simpset() addsimps [pnat_add_commute]) 1);
-(*j moves to the end because it is free while k, l are bound*)
-by (etac pnat_add_le_mono1 1);
-qed "pnad_add_le_mono";
-
 Goal "1 * Rep_pnat n = Rep_pnat n";
 by (Asm_simp_tac 1);
 qed "Rep_pnat_mult_1";
@@ -489,8 +373,7 @@
 by (Asm_simp_tac 1);
 qed "Rep_pnat_mult_1_right";
 
-Goal
-      "(Rep_pnat x * Rep_pnat y): pnat";
+Goal "(Rep_pnat x * Rep_pnat y): pnat";
 by (cut_facts_tac [[Rep_pnat_gt_zero,
     Rep_pnat_gt_zero] MRS mult_less_mono1,Collect_pnat_gt_0] 1);
 by (etac ssubst 1);
@@ -499,8 +382,7 @@
 
 Goalw [pnat_mult_def] 
       "Rep_pnat x * Rep_pnat y = Rep_pnat (x * y)";
-by (simp_tac (simpset() addsimps [mult_Rep_pnat RS 
-                          Abs_pnat_inverse]) 1);
+by (simp_tac (simpset() addsimps [mult_Rep_pnat RS Abs_pnat_inverse]) 1);
 qed "mult_Rep_pnat_mult";
 
 Goalw [pnat_mult_def] "m * n = n * (m::pnat)";
diff -r a81ea5d3dd41 -r c4f1bf2acf4c src/HOL/Real/PRat.ML
--- a/src/HOL/Real/PRat.ML	Sat Dec 30 22:03:47 2000 +0100
+++ b/src/HOL/Real/PRat.ML	Sat Dec 30 22:13:18 2000 +0100
@@ -614,21 +614,11 @@
 by (fast_tac (claset() addIs [prat_less_trans]) 1);
 qed "prat_le_less_trans";
 
-Goal "!! (i::prat). [| i < j; j <= k |] ==> i < k";
-by (dtac prat_le_imp_less_or_eq 1);
-by (fast_tac (claset() addIs [prat_less_trans]) 1);
-qed "prat_less_le_trans";
-
 Goal "[| i <= j; j <= k |] ==> i <= (k::prat)";
 by (EVERY1 [dtac prat_le_imp_less_or_eq, dtac prat_le_imp_less_or_eq,
             rtac prat_less_or_eq_imp_le, fast_tac (claset() addIs [prat_less_trans])]);
 qed "prat_le_trans";
 
-Goal "[| z <= w; w <= z |] ==> z = (w::prat)";
-by (EVERY1 [dtac prat_le_imp_less_or_eq, dtac prat_le_imp_less_or_eq,
-            fast_tac (claset() addEs [prat_less_irrefl,prat_less_asym])]);
-qed "prat_le_anti_sym";
-
 Goal "[| ~ y < x; y ~= x |] ==> x < (y::prat)";
 by (rtac not_prat_leE 1);
 by (fast_tac (claset() addDs [prat_le_imp_less_or_eq]) 1);
diff -r a81ea5d3dd41 -r c4f1bf2acf4c src/HOL/Real/PReal.ML
--- a/src/HOL/Real/PReal.ML	Sat Dec 30 22:03:47 2000 +0100
+++ b/src/HOL/Real/PReal.ML	Sat Dec 30 22:13:18 2000 +0100
@@ -158,7 +158,7 @@
 qed "preal_less_not_refl";
 
 (*** y < y ==> P ***)
-bind_thm("preal_less_irrefl",preal_less_not_refl RS notE);
+bind_thm("preal_less_irrefl", preal_less_not_refl RS notE);
 
 Goal "!!(x::preal). x < y ==> x ~= y";
 by (auto_tac (claset(),simpset() addsimps [preal_less_not_refl]));
@@ -750,17 +750,17 @@
 qed "preal_less_le_iff";
 
 Goalw [preal_le_def,preal_less_def,psubset_def] 
-                  "z < w ==> z <= (w::preal)";
+     "z < w ==> z <= (w::preal)";
 by (Fast_tac 1);
 qed "preal_less_imp_le";
 
 Goalw [preal_le_def,preal_less_def,psubset_def] 
-                      "!!(x::preal). x <= y ==> x < y | x = y";
+     "!!(x::preal). x <= y ==> x < y | x = y";
 by (auto_tac (claset() addIs [inj_Rep_preal RS injD],simpset()));
 qed "preal_le_imp_less_or_eq";
 
 Goalw [preal_le_def,preal_less_def,psubset_def] 
-                       "!!(x::preal). x < y | x = y ==> x <=y";
+     "!!(x::preal). x < y | x = y ==> x <=y";
 by Auto_tac;
 qed "preal_less_or_eq_imp_le";
 
@@ -768,19 +768,10 @@
 by (Simp_tac 1);
 qed "preal_le_refl";
 
-Goal "[| i <= j; j < k |] ==> i < (k::preal)";
-by (dtac preal_le_imp_less_or_eq 1);
-by (fast_tac (claset() addIs [preal_less_trans]) 1);
-qed "preal_le_less_trans";
-
-Goal "[| i < j; j <= k |] ==> i < (k::preal)";
-by (dtac preal_le_imp_less_or_eq 1);
-by (fast_tac (claset() addIs [preal_less_trans]) 1);
-qed "preal_less_le_trans";
-
 Goal "[| i <= j; j <= k |] ==> i <= (k::preal)";
 by (EVERY1 [dtac preal_le_imp_less_or_eq, dtac preal_le_imp_less_or_eq,
-            rtac preal_less_or_eq_imp_le, fast_tac (claset() addIs [preal_less_trans])]);
+          rtac preal_less_or_eq_imp_le, 
+                 fast_tac (claset() addIs [preal_less_trans])]);
 qed "preal_le_trans";
 
 Goal "[| z <= w; w <= z |] ==> z = (w::preal)";
@@ -788,10 +779,17 @@
             fast_tac (claset() addEs [preal_less_irrefl,preal_less_asym])]);
 qed "preal_le_anti_sym";
 
-Goal "[| ~ y < x; y ~= x |] ==> x < (y::preal)";
-by (rtac not_preal_leE 1);
-by (fast_tac (claset() addDs [preal_le_imp_less_or_eq]) 1);
-qed "not_less_not_eq_preal_less";
+Goal "!!w::preal. (w ~= z) = (w<z | z<w)";
+by (cut_inst_tac [("r1.0","w"),("r2.0","z")] preal_linear 1);
+by (auto_tac (claset() addEs [preal_less_irrefl], simpset()));
+qed "preal_neq_iff";
+
+(* Axiom 'order_less_le' of class 'order': *)
+Goal "(w::preal) < z = (w <= z & w ~= z)";
+by (simp_tac (simpset() addsimps [preal_less_le_iff RS sym, preal_neq_iff]) 1);
+by (blast_tac (claset() addSEs [preal_less_asym]) 1);
+qed "preal_less_le";
+
 
 (****)(****)(****)(****)(****)(****)(****)(****)(****)(****)(****)(****)
 
@@ -833,9 +831,7 @@
 by (auto_tac (claset(),simpset() addsimps [prat_less_def]));
 qed "lemma_ex_mem_less_left_add1";
 
-Goal
-     "A < B ==> \
-\       {} < {d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}";
+Goal "A < B ==> {} < {d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}";
 by (dtac lemma_ex_mem_less_left_add1 1);
 by (auto_tac (claset() addSIs [psubsetI] addEs [equalityCE],simpset()));
 qed "preal_less_set_not_empty";
@@ -860,7 +856,7 @@
 
 (** Part 3 of Dedekind sections def **)
 Goal "A < B ==> ALL y: {d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}. \
- \      ALL z. z < y --> z : {d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}";
+ \   ALL z. z < y --> z : {d. EX n. n ~: Rep_preal(A) & n + d : Rep_preal(B)}";
 by Auto_tac;
 by (dres_inst_tac [("x","n")] prat_add_less2_mono2 1);
 by (dtac (Rep_preal RS prealE_lemma3b) 1);
@@ -979,8 +975,8 @@
 by (dtac preal_le_imp_less_or_eq 1);
 by (Step_tac 1);
 by (auto_tac (claset() addSIs [preal_le_refl,
-    preal_less_imp_le,preal_add_less2_mono1],
-    simpset() addsimps [preal_add_commute]));
+                               preal_less_imp_le,preal_add_less2_mono1],
+              simpset() addsimps [preal_add_commute]));
 qed "preal_add_left_le_mono1";
 
 Goal "!!(q1::preal). q1 <= q2  ==> q1 + x <= q2 + x";
diff -r a81ea5d3dd41 -r c4f1bf2acf4c src/HOL/Real/RComplete.ML
--- a/src/HOL/Real/RComplete.ML	Sat Dec 30 22:03:47 2000 +0100
+++ b/src/HOL/Real/RComplete.ML	Sat Dec 30 22:13:18 2000 +0100
@@ -8,6 +8,10 @@
 
 claset_ref() := claset() delWrapper "bspec";
 
+Goal "x/#2 + x/#2 = (x::real)";
+by (Simp_tac 1);
+qed "real_sum_of_halves";
+
 (*---------------------------------------------------------
        Completeness of reals: use supremum property of 
        preal and theorems about real_preal. Theorems 
@@ -30,7 +34,7 @@
 by Auto_tac;
 by (dtac bspec 1 THEN assume_tac 1);
 by (ftac bspec 1  THEN assume_tac 1);
-by (dtac real_less_trans 1 THEN assume_tac 1);
+by (dtac order_less_trans 1 THEN assume_tac 1);
 by (dtac ((rename_numerals real_gt_zero_preal_Ex) RS iffD1) 1
     THEN etac exE 1);    
 by (res_inst_tac [("x","ya")] exI 1);
@@ -137,14 +141,6 @@
 by (Auto_tac);
 qed "lemma_le_swap2";
 
-Goal "[| (x::real) + (-X) + #1 <= S; xa < x |] ==> xa + (-X) + #1 <= S";
-by (Auto_tac);
-qed "lemma_real_complete2";
-
-Goal "[| (x::real) + (-X) + #1 <= S; xa < x |] ==> xa <= S + X + (-#1)"; (**)
-by (Auto_tac);
-qed "lemma_real_complete2a";
-
 Goal "[| (x::real) + (-X) + #1 <= S; xa <= x |] ==> xa <= S + X + (-#1)";
 by (Auto_tac);
 qed "lemma_real_complete2b";
@@ -184,7 +180,7 @@
 by (ftac isLubD2 1 THEN assume_tac 2);
 by (Blast_tac 1);
 by (rtac lemma_real_complete2b 1);
-by (etac real_less_imp_le 2);
+by (etac order_less_imp_le 2);
 by (blast_tac (claset() addSIs [isLubD2]) 1 THEN Step_tac 1);
 by (full_simp_tac (simpset() addsimps [real_add_assoc]) 1);
 by (blast_tac (claset() addDs [isUbD] addSIs [setleI RS isUbI]
@@ -218,16 +214,16 @@
 by (blast_tac (claset() addSIs [isUbI,setleI]) 2);
 by (dres_inst_tac [("y","t+(-x)")] isLub_le_isUb 1);
 by (dres_inst_tac [("x","-t")] real_add_left_le_mono1 2);
-by (auto_tac (claset() addDs [real_le_less_trans,
-			      (real_minus_zero_less_iff2 RS iffD2)], 
-	      simpset() addsimps [real_less_not_refl,real_add_assoc RS sym]));
+by (auto_tac (claset() addDs [order_le_less_trans,
+			      real_minus_zero_less_iff2 RS iffD2], 
+	      simpset() addsimps [real_add_assoc RS sym]));
 qed "reals_Archimedean";
 
 Goal "EX n. (x::real) < real_of_posnat n";
 by (res_inst_tac [("R1.0","x"),("R2.0","#0")] real_linear_less2 1);
 by (res_inst_tac [("x","0")] exI 1);
 by (res_inst_tac [("x","0")] exI 2);
-by (auto_tac (claset() addEs [real_less_trans],
+by (auto_tac (claset() addEs [order_less_trans],
 	      simpset() addsimps [real_of_posnat_one,real_zero_less_one]));
 by (ftac ((rename_numerals real_inverse_gt_zero) RS reals_Archimedean) 1);
 by (Step_tac 1 THEN res_inst_tac [("x","n")] exI 1);
diff -r a81ea5d3dd41 -r c4f1bf2acf4c src/HOL/Real/ROOT.ML
--- a/src/HOL/Real/ROOT.ML	Sat Dec 30 22:03:47 2000 +0100
+++ b/src/HOL/Real/ROOT.ML	Sat Dec 30 22:13:18 2000 +0100
@@ -3,9 +3,8 @@
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1998  University of Cambridge
 
-Construction of the Reals using Dedekind Cuts, Ultrapower Construction
-of the hyperreals, and mechanization of Nonstandard Real Analysis
-                        by Jacques Fleuriot
+Construction of the Reals using Dedekind Cuts 
+by Jacques Fleuriot
 *)
 
-with_path "Hyperreal" time_use_thy "Hyperreal";
+time_use_thy "Real";
diff -r a81ea5d3dd41 -r c4f1bf2acf4c src/HOL/Real/RealAbs.ML
--- a/src/HOL/Real/RealAbs.ML	Sat Dec 30 22:03:47 2000 +0100
+++ b/src/HOL/Real/RealAbs.ML	Sat Dec 30 22:13:18 2000 +0100
@@ -49,11 +49,11 @@
 by (Asm_simp_tac 1);
 qed "abs_eqI1";
 
-Goalw [real_abs_def] "(#0::real)<x ==> abs x = x";
+Goalw [real_abs_def] "(#0::real) < x ==> abs x = x";
 by (Asm_simp_tac 1);
 qed "abs_eqI2";
 
-Goalw [real_abs_def,real_le_def] "x<(#0::real) ==> abs x = -x";
+Goalw [real_abs_def,real_le_def] "x < (#0::real) ==> abs x = -x";
 by (Asm_simp_tac 1);
 qed "abs_minus_eqI2";
 
@@ -130,62 +130,41 @@
 qed "abs_add_minus_less";
 
 (* lemmas manipulating terms *)
-Goal "((#0::real)*x<r)=(#0<r)";
+Goal "((#0::real)*x < r)=(#0 < r)";
 by (Simp_tac 1);
 qed "real_mult_0_less";
 
-Goal "[| (#0::real)<y; x<r; y*r<t*s |] ==> y*x<t*s";
+Goal "[| (#0::real) < y; x < r; y*r < t*s |] ==> y*x < t*s";
 by (blast_tac (claset() addSIs [rename_numerals real_mult_less_mono2] 
-                        addIs  [real_less_trans]) 1);
+                        addIs  [order_less_trans]) 1);
 qed "real_mult_less_trans";
 
-Goal "[| (#0::real)<=y; x<r; y*r<t*s; #0<t*s|] ==> y*x<t*s";
-by (dtac real_le_imp_less_or_eq 1);
+Goal "[| (#0::real)<=y; x < r; y*r < t*s; #0 < t*s|] ==> y*x < t*s";
+by (dtac order_le_imp_less_or_eq 1);
 by (fast_tac (HOL_cs addEs [real_mult_0_less RS iffD2,
 			    real_mult_less_trans]) 1);
 qed "real_mult_le_less_trans";
 
-Goal "[| abs x<r; abs y<s |] ==> abs(x*y)<r*(s::real)";
+Goal "[| abs x < r; abs y < s |] ==> abs(x*y) < r*(s::real)";
 by (simp_tac (simpset() addsimps [abs_mult]) 1);
 by (rtac real_mult_le_less_trans 1);
 by (rtac abs_ge_zero 1);
 by (assume_tac 1);
 by (rtac (rename_numerals real_mult_order) 2);
-by (auto_tac (claset() addSIs [real_mult_less_mono1,
-    abs_ge_zero] addIs [real_le_less_trans],simpset()));
+by (auto_tac (claset() addSIs [real_mult_less_mono1, abs_ge_zero] 
+                       addIs [order_le_less_trans],
+              simpset()));
 qed "abs_mult_less";
 
-Goal "[| abs x < r; abs y < s |] ==> abs(x)*abs(y)<r*(s::real)";
+Goal "[| abs x < r; abs y < s |] ==> abs(x)*abs(y) < r*(s::real)";
 by (auto_tac (claset() addIs [abs_mult_less],
               simpset() addsimps [abs_mult RS sym]));
 qed "abs_mult_less2";
 
-Goal "(#1::real) < abs x ==> abs y <= abs(x*y)";
-by (cut_inst_tac [("x1","y")] (abs_ge_zero RS real_le_imp_less_or_eq) 1);
-by (EVERY1[etac disjE,rtac real_less_imp_le]);
-by (dres_inst_tac [("W","#1")]  real_less_sum_gt_zero 1);
-by (forw_inst_tac [("y","abs x + (-#1)")] 
-    (rename_numerals real_mult_order) 1);
-by (rtac real_sum_gt_zero_less 2);
-by (asm_full_simp_tac (simpset() 
-    addsimps [real_add_mult_distrib2,
-    real_mult_commute, abs_mult]) 2);
-by (dtac sym 2);
-by (auto_tac (claset(),simpset() addsimps [abs_mult]));
-qed "abs_mult_le";
-
-Goal "[| (#1::real) < abs x; r < abs y|] ==> r < abs(x*y)";
-by (blast_tac (HOL_cs addIs [abs_mult_le, real_less_le_trans]) 1);
-qed "abs_mult_gt";
-
-Goal "abs(x)<r ==> (#0::real)<r";
-by (blast_tac (claset() addSIs [real_le_less_trans,abs_ge_zero]) 1);
+Goal "abs(x) < r ==> (#0::real) < r";
+by (blast_tac (claset() addSIs [order_le_less_trans,abs_ge_zero]) 1);
 qed "abs_less_gt_zero";
 
-Goalw [real_abs_def] "abs #1 = (#1::real)";
-by (Simp_tac 1);
-qed "abs_one";
-
 Goalw [real_abs_def] "abs (-#1) = (#1::real)";
 by (Simp_tac 1);
 qed "abs_minus_one";
@@ -195,7 +174,7 @@
 by Auto_tac;
 qed "abs_disj";
 
-Goalw [real_abs_def] "(abs x < r) = (-r<x & x<(r::real))";
+Goalw [real_abs_def] "(abs x < r) = (-r < x & x < (r::real))";
 by Auto_tac;
 qed "abs_interval_iff";
 
@@ -219,7 +198,7 @@
 Addsimps [abs_not_less_zero];
 
 Goal "abs h < abs y - abs x ==> abs (x + h) < abs (y::real)";
-by (auto_tac (claset() addIs [abs_triangle_ineq RS real_le_less_trans], 
+by (auto_tac (claset() addIs [abs_triangle_ineq RS order_le_less_trans], 
     simpset()));
 qed "abs_circle";
 
@@ -242,13 +221,13 @@
 
 Goal "~ abs(x) + (#1::real) < x";
 by (rtac real_leD 1);
-by (auto_tac (claset() addIs [abs_ge_self RS real_le_trans], simpset()));
+by (auto_tac (claset() addIs [abs_ge_self RS order_trans], simpset()));
 qed "abs_add_one_not_less_self";
 Addsimps [abs_add_one_not_less_self];
  
 (* used in vector theory *)
 Goal "abs(w + x + (y::real)) <= abs(w) + abs(x) + abs(y)";
-by (auto_tac (claset() addSIs [abs_triangle_ineq RS real_le_trans,
+by (auto_tac (claset() addSIs [abs_triangle_ineq RS order_trans,
                                real_add_left_le_mono1],
               simpset() addsimps [real_add_assoc]));
 qed "abs_triangle_ineq_three";
diff -r a81ea5d3dd41 -r c4f1bf2acf4c src/HOL/Real/RealArith0.ML
--- a/src/HOL/Real/RealArith0.ML	Sat Dec 30 22:03:47 2000 +0100
+++ b/src/HOL/Real/RealArith0.ML	Sat Dec 30 22:13:18 2000 +0100
@@ -22,7 +22,7 @@
               simpset() addsimps [linorder_neq_iff, 
                                   rename_numerals real_inverse_gt_zero]));  
 qed "real_0_less_inverse_iff";
-AddIffs [real_0_less_inverse_iff];
+Addsimps [real_0_less_inverse_iff];
 
 Goal "(inverse x < (#0::real)) = (x < #0)";
 by (case_tac "x=#0" 1);
@@ -31,34 +31,23 @@
               simpset() addsimps [linorder_neq_iff, 
                                   rename_numerals real_inverse_gt_zero]));  
 qed "real_inverse_less_0_iff";
-AddIffs [real_inverse_less_0_iff];
+Addsimps [real_inverse_less_0_iff];
 
 Goal "((#0::real) <= inverse x) = (#0 <= x)";
 by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1); 
 qed "real_0_le_inverse_iff";
-AddIffs [real_0_le_inverse_iff];
+Addsimps [real_0_le_inverse_iff];
 
 Goal "(inverse x <= (#0::real)) = (x <= #0)";
 by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1); 
 qed "real_inverse_le_0_iff";
-AddIffs [real_inverse_le_0_iff];
+Addsimps [real_inverse_le_0_iff];
 
 Goalw [real_divide_def] "x/(#0::real) = #0";
 by (stac (rename_numerals INVERSE_ZERO) 1); 
 by (Simp_tac 1); 
 qed "REAL_DIVIDE_ZERO";
 
-(*generalize?*)
-Goal "((#0::real) < #1/x) = (#0 < x)";
-by (simp_tac (simpset() addsimps [real_divide_def]) 1);
-qed "real_0_less_recip_iff";
-AddIffs [real_0_less_recip_iff];
-
-Goal "(#1/x < (#0::real)) = (x < #0)";
-by (simp_tac (simpset() addsimps [real_divide_def]) 1);
-qed "real_recip_less_0_iff";
-AddIffs [real_recip_less_0_iff];
-
 Goal "inverse (x::real) = #1/x";
 by (simp_tac (simpset() addsimps [real_divide_def]) 1); 
 qed "real_inverse_eq_divide";
@@ -90,12 +79,12 @@
 by (rtac ccontr 1); 
 by (blast_tac (claset() addDs [rename_numerals real_inverse_not_zero]) 1); 
 qed "real_inverse_zero_iff";
-AddIffs [real_inverse_zero_iff];
+Addsimps [real_inverse_zero_iff];
 
 Goal "(x/y = #0) = (x=#0 | y=(#0::real))";
 by (auto_tac (claset(), simpset() addsimps [real_divide_def]));  
 qed "real_divide_eq_0_iff";
-AddIffs [real_divide_eq_0_iff];
+Addsimps [real_divide_eq_0_iff];
 
 
 (**** Factor cancellation theorems for "real" ****)
@@ -259,7 +248,7 @@
   val neg_exchanges = true
 )
 
-val real_cancel_numeral_factors = 
+val real_cancel_numeral_factors_relations = 
   map prep_simproc
    [("realeq_cancel_numeral_factor",
      prep_pats ["(l::real) * m = n", "(l::real) = m * n"], 
@@ -269,10 +258,16 @@
      LessCancelNumeralFactor.proc),
     ("realle_cancel_numeral_factor", 
      prep_pats ["(l::real) * m <= n", "(l::real) <= m * n"], 
-     LeCancelNumeralFactor.proc),
-    ("realdiv_cancel_numeral_factor", 
-     prep_pats ["((l::real) * m) / n", "(l::real) / (m * n)"], 
-     DivCancelNumeralFactor.proc)];
+     LeCancelNumeralFactor.proc)];
+
+val real_cancel_numeral_factors_divide = prep_simproc
+	("realdiv_cancel_numeral_factor", 
+	 prep_pats ["((l::real) * m) / n", "(l::real) / (m * n)"], 
+	 DivCancelNumeralFactor.proc);
+
+val real_cancel_numeral_factors = 
+    real_cancel_numeral_factors_relations @ 
+    [real_cancel_numeral_factors_divide];
 
 end;
 
@@ -624,7 +619,8 @@
 AddIffs [real_0_le_diff_iff];
 
 (*
-?? still needed ??
+FIXME: we should have this, as for type int, but many proofs would break.
+It replaces x+-y by x-y.
 Addsimps [symmetric real_diff_def];
 *)
 
diff -r a81ea5d3dd41 -r c4f1bf2acf4c src/HOL/Real/RealBin.ML
--- a/src/HOL/Real/RealBin.ML	Sat Dec 30 22:03:47 2000 +0100
+++ b/src/HOL/Real/RealBin.ML	Sat Dec 30 22:13:18 2000 +0100
@@ -82,7 +82,7 @@
 \     iszero (number_of (bin_add v (bin_minus v')))";
 by (simp_tac
     (HOL_ss addsimps [real_number_of_def, 
-				  real_of_int_eq_iff, eq_number_of_eq]) 1);
+	              real_of_int_eq_iff, eq_number_of_eq]) 1);
 qed "eq_real_number_of";
 
 Addsimps [eq_real_number_of];
@@ -148,6 +148,11 @@
 bind_thm ("real_mult_le_0_iff", 
 	  rename_numerals real_mult_le_zero_iff);
 
+bind_thm ("real_inverse_less_0", rename_numerals real_inverse_less_zero);
+bind_thm ("real_inverse_gt_0", rename_numerals real_inverse_gt_zero);
+
+Addsimps [rename_numerals real_le_square];
+
 
 (*Perhaps add some theorems that aren't in the default simpset, as
   done in Integ/NatBin.ML*)
diff -r a81ea5d3dd41 -r c4f1bf2acf4c src/HOL/Real/RealDef.ML
--- a/src/HOL/Real/RealDef.ML	Sat Dec 30 22:03:47 2000 +0100
+++ b/src/HOL/Real/RealDef.ML	Sat Dec 30 22:13:18 2000 +0100
@@ -543,8 +543,6 @@
 by (asm_full_simp_tac (simpset() addsimps [real_mult_assoc RS sym]) 1);
 qed "real_mult_not_zero";
 
-bind_thm ("real_mult_not_zeroE",real_mult_not_zero RS notE);
-
 Goal "inverse(inverse (x::real)) = x";
 by (real_div_undefined_case_tac "x=0" 1);
 by (res_inst_tac [("c1","inverse x")] (real_mult_right_cancel RS iffD1) 1);
@@ -656,8 +654,8 @@
 by (res_inst_tac [("z","R")] eq_Abs_real 1);
 by (auto_tac (claset(),simpset() addsimps [real_less_def]));
 by (dtac preal_lemma_for_not_refl 1);
-by (assume_tac 1 THEN rotate_tac 2 1);
-by (auto_tac (claset(),simpset() addsimps [preal_less_not_refl]));
+by (assume_tac 1);
+by Auto_tac;
 qed "real_less_not_refl";
 
 (*** y < y ==> P ***)
@@ -936,10 +934,6 @@
 by (Blast_tac 1);
 qed "not_real_leE";
 
-Goalw [real_le_def] "z < w ==> z <= (w::real)";
-by (blast_tac (claset() addEs [real_less_asym]) 1);
-qed "real_less_imp_le";
-
 Goalw [real_le_def] "!!(x::real). x <= y ==> x < y | x = y";
 by (cut_facts_tac [real_linear] 1);
 by (blast_tac (claset() addEs [real_less_irrefl,real_less_asym]) 1);
@@ -958,8 +952,6 @@
 by (simp_tac (simpset() addsimps [real_le_less]) 1);
 qed "real_le_refl";
 
-AddIffs [real_le_refl];
-
 (* Axiom 'linorder_linear' of class 'linorder': *)
 Goal "(z::real) <= w | w <= z";
 by (simp_tac (simpset() addsimps [real_le_less]) 1);
@@ -967,19 +959,10 @@
 by (Blast_tac 1);
 qed "real_le_linear";
 
-Goal "[| i <= j; j < k |] ==> i < (k::real)";
-by (dtac real_le_imp_less_or_eq 1);
-by (blast_tac (claset() addIs [real_less_trans]) 1);
-qed "real_le_less_trans";
-
-Goal "!! (i::real). [| i < j; j <= k |] ==> i < k";
-by (dtac real_le_imp_less_or_eq 1);
-by (blast_tac (claset() addIs [real_less_trans]) 1);
-qed "real_less_le_trans";
-
 Goal "[| i <= j; j <= k |] ==> i <= (k::real)";
 by (EVERY1 [dtac real_le_imp_less_or_eq, dtac real_le_imp_less_or_eq,
-            rtac real_less_or_eq_imp_le, blast_tac (claset() addIs [real_less_trans])]);
+            rtac real_less_or_eq_imp_le, 
+            blast_tac (claset() addIs [real_less_trans])]);
 qed "real_le_trans";
 
 Goal "[| z <= w; w <= z |] ==> z = (w::real)";
diff -r a81ea5d3dd41 -r c4f1bf2acf4c src/HOL/Real/RealDef.thy
--- a/src/HOL/Real/RealDef.thy	Sat Dec 30 22:03:47 2000 +0100
+++ b/src/HOL/Real/RealDef.thy	Sat Dec 30 22:13:18 2000 +0100
@@ -7,6 +7,9 @@
 
 RealDef = PReal +
 
+instance preal :: order (preal_le_refl,preal_le_trans,preal_le_anti_sym,
+                         preal_less_le)
+
 constdefs
   realrel   ::  "((preal * preal) * (preal * preal)) set"
   "realrel == {p. ? x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1}" 
@@ -18,8 +21,11 @@
    real  :: {ord, zero, plus, times, minus, inverse}
 
 consts 
+  "1r"   :: real               ("1r")  
 
-  "1r"       :: real               ("1r")  
+   (*Overloaded constant: denotes the Real subset of enclosing types such as
+     hypreal and complex*)
+   SReal :: "'a set"
 
 defs
 
@@ -58,18 +64,21 @@
 defs
 
   real_add_def  
-  "P + Q == Abs_real(UN p1:Rep_real(P). UN p2:Rep_real(Q).
-                (%(x1,y1). (%(x2,y2). realrel^^{(x1+x2, y1+y2)}) p2) p1)"
+  "P+Q == Abs_real(UN p1:Rep_real(P). UN p2:Rep_real(Q).
+                   (%(x1,y1). (%(x2,y2). realrel^^{(x1+x2, y1+y2)}) p2) p1)"
   
   real_mult_def  
-  "P * Q == Abs_real(UN p1:Rep_real(P). UN p2:Rep_real(Q).
-                (%(x1,y1). (%(x2,y2). realrel^^{(x1*x2+y1*y2,x1*y2+x2*y1)}) p2) p1)"
+  "P*Q == Abs_real(UN p1:Rep_real(P). UN p2:Rep_real(Q).
+                   (%(x1,y1). (%(x2,y2). realrel^^{(x1*x2+y1*y2,x1*y2+x2*y1)})
+		   p2) p1)"
 
   real_less_def
-  "P < Q == EX x1 y1 x2 y2. x1 + y2 < x2 + y1 & 
-                                   (x1,y1):Rep_real(P) &
-                                   (x2,y2):Rep_real(Q)" 
+  "P<Q == EX x1 y1 x2 y2. x1 + y2 < x2 + y1 & 
+                            (x1,y1):Rep_real(P) & (x2,y2):Rep_real(Q)" 
   real_le_def
   "P <= (Q::real) == ~(Q < P)"
 
+syntax (symbols)
+  SReal     :: "'a set"                   ("\\<real>")
+
 end
diff -r a81ea5d3dd41 -r c4f1bf2acf4c src/HOL/Real/RealOrd.ML
--- a/src/HOL/Real/RealOrd.ML	Sat Dec 30 22:03:47 2000 +0100
+++ b/src/HOL/Real/RealOrd.ML	Sat Dec 30 22:13:18 2000 +0100
@@ -78,16 +78,16 @@
 
 Goal "real_of_preal z < x ==> EX y. x = real_of_preal y";
 by (blast_tac (claset() addSDs [real_of_preal_zero_less RS real_less_trans]
-               addIs [real_gt_zero_preal_Ex RS iffD1]) 1);
+                        addIs [real_gt_zero_preal_Ex RS iffD1]) 1);
 qed "real_gt_preal_preal_Ex";
 
 Goal "real_of_preal z <= x ==> EX y. x = real_of_preal y";
-by (blast_tac (claset() addDs [real_le_imp_less_or_eq,
+by (blast_tac (claset() addDs [order_le_imp_less_or_eq,
 			       real_gt_preal_preal_Ex]) 1);
 qed "real_ge_preal_preal_Ex";
 
 Goal "y <= 0 ==> ALL x. y < real_of_preal x";
-by (auto_tac (claset() addEs [real_le_imp_less_or_eq RS disjE]
+by (auto_tac (claset() addEs [order_le_imp_less_or_eq RS disjE]
                        addIs [real_of_preal_zero_less RSN(2,real_less_trans)],
               simpset() addsimps [real_of_preal_zero_less]));
 qed "real_less_all_preal";
@@ -113,8 +113,8 @@
 
 Goal "(real_of_preal m1 <= real_of_preal m2) = (m1 <= m2)";
 by (auto_tac (claset() addSIs [preal_leI],
-    simpset() addsimps [real_less_le_iff RS sym]));
-by (dtac preal_le_less_trans 1 THEN assume_tac 1);
+              simpset() addsimps [real_less_le_iff RS sym]));
+by (dtac order_le_less_trans 1 THEN assume_tac 1);
 by (etac preal_less_irrefl 1);
 qed "real_of_preal_le_iff";
 
@@ -131,28 +131,28 @@
 qed "real_mult_less_zero1";
 
 Goal "[| 0 <= x; 0 <= y |] ==> (0::real) <= x * y";
-by (REPEAT(dtac real_le_imp_less_or_eq 1));
-by (auto_tac (claset() addIs [real_mult_order, real_less_imp_le],
+by (REPEAT(dtac order_le_imp_less_or_eq 1));
+by (auto_tac (claset() addIs [real_mult_order, order_less_imp_le],
 	      simpset()));
 qed "real_le_mult_order";
 
 Goal "[| 0 < x; 0 <= y |] ==> (0::real) <= x * y";
-by (dtac real_le_imp_less_or_eq 1);
-by (auto_tac (claset() addIs [real_mult_order,
-			      real_less_imp_le],simpset()));
+by (dtac order_le_imp_less_or_eq 1);
+by (auto_tac (claset() addIs [real_mult_order, order_less_imp_le], 
+              simpset()));
 qed "real_less_le_mult_order";
 
 Goal "[| x <= 0; y <= 0 |] ==> (0::real) <= x * y";
 by (rtac real_less_or_eq_imp_le 1);
-by (dtac real_le_imp_less_or_eq 1 THEN etac disjE 1);
+by (dtac order_le_imp_less_or_eq 1 THEN etac disjE 1);
 by Auto_tac;
-by (dtac real_le_imp_less_or_eq 1);
+by (dtac order_le_imp_less_or_eq 1);
 by (auto_tac (claset() addDs [real_mult_less_zero1],simpset()));
 qed "real_mult_le_zero1";
 
 Goal "[| 0 <= x; y < 0 |] ==> x * y <= (0::real)";
 by (rtac real_less_or_eq_imp_le 1);
-by (dtac real_le_imp_less_or_eq 1 THEN etac disjE 1);
+by (dtac order_le_imp_less_or_eq 1 THEN etac disjE 1);
 by Auto_tac;
 by (dtac (real_minus_zero_less_iff RS iffD2) 1);
 by (rtac (real_minus_zero_less_iff RS subst) 1);
@@ -201,12 +201,12 @@
 bind_thm ("real_add_le_mono1", real_add_right_cancel_le RS iffD2);
 
 Goal "!!z z'::real. [| w'<w; z'<=z |] ==> w' + z' < w + z";
-by (etac (real_add_less_mono1 RS real_less_le_trans) 1);
+by (etac (real_add_less_mono1 RS order_less_le_trans) 1);
 by (Simp_tac 1);
 qed "real_add_less_le_mono";
 
 Goal "!!z z'::real. [| w'<=w; z'<z |] ==> w' + z' < w + z";
-by (etac (real_add_le_mono1 RS real_le_less_trans) 1);
+by (etac (real_add_le_mono1 RS order_le_less_trans) 1);
 by (Simp_tac 1);
 qed "real_add_le_less_mono";
 
@@ -231,20 +231,20 @@
 qed "real_le_add_left_cancel";
 
 Goal "[| 0 < x; 0 < y |] ==> (0::real) < x + y";
-by (etac real_less_trans 1);
+by (etac order_less_trans 1);
 by (dtac real_add_less_mono2 1);
 by (Full_simp_tac 1);
 qed "real_add_order";
 
 Goal "[| 0 <= x; 0 <= y |] ==> (0::real) <= x + y";
-by (REPEAT(dtac real_le_imp_less_or_eq 1));
-by (auto_tac (claset() addIs [real_add_order, real_less_imp_le],
+by (REPEAT(dtac order_le_imp_less_or_eq 1));
+by (auto_tac (claset() addIs [real_add_order, order_less_imp_le],
 	      simpset()));
 qed "real_le_add_order";
 
 Goal "[| R1 < S1; R2 < S2 |] ==> R1 + R2 < S1 + (S2::real)";
 by (dtac real_add_less_mono1 1);
-by (etac real_less_trans 1);
+by (etac order_less_trans 1);
 by (etac real_add_less_mono2 1);
 qed "real_add_less_mono";
 
@@ -254,7 +254,7 @@
 
 Goal "[|i<=j;  k<=l |] ==> i + k <= j + (l::real)";
 by (dtac real_add_le_mono1 1);
-by (etac real_le_trans 1);
+by (etac order_trans 1);
 by (Simp_tac 1);
 qed "real_add_le_mono";
 
@@ -283,14 +283,14 @@
 Addsimps [real_le_minus_iff];
           
 Goal "0 <= 1r";
-by (rtac (real_zero_less_one RS real_less_imp_le) 1);
+by (rtac (real_zero_less_one RS order_less_imp_le) 1);
 qed "real_zero_le_one";
 Addsimps [real_zero_le_one];
 
 Goal "(0::real) <= x*x";
 by (res_inst_tac [("R2.0","0"),("R1.0","x")] real_linear_less2 1);
 by (auto_tac (claset() addIs [real_mult_order,
-			      real_mult_less_zero1,real_less_imp_le],
+			      real_mult_less_zero1,order_less_imp_le],
 	      simpset()));
 qed "real_le_square";
 Addsimps [real_le_square];
@@ -353,7 +353,7 @@
 by (induct_tac "n" 1);
 by (auto_tac (claset(),
 	      simpset () addsimps [real_of_posnat_Suc,real_of_posnat_one,
-			   real_of_posnat_gt_zero, real_less_imp_le]));
+			   real_of_posnat_gt_zero, order_less_imp_le]));
 qed "real_of_posnat_less_one";
 Addsimps [real_of_posnat_less_one];
 
@@ -378,7 +378,7 @@
 by (forward_tac [real_minus_zero_less_iff2 RS iffD2] 1);
 by (forward_tac [real_not_refl2 RS not_sym] 1);
 by (dtac (real_not_refl2 RS not_sym RS real_inverse_not_zero) 1);
-by (EVERY1[dtac real_le_imp_less_or_eq, Step_tac]); 
+by (EVERY1[dtac order_le_imp_less_or_eq, Step_tac]); 
 by (dtac real_mult_less_zero1 1 THEN assume_tac 1);
 by (auto_tac (claset() addIs [real_zero_less_one RS real_less_asym],
 	      simpset()));
@@ -418,40 +418,33 @@
 qed "real_one_less_two";
 
 Goal "0 < 1r + 1r";
-by (rtac ([real_zero_less_one,
-	   real_one_less_two] MRS real_less_trans) 1);
+by (rtac ([real_zero_less_one, real_one_less_two] MRS order_less_trans) 1);
 qed "real_zero_less_two";
 
 Goal "1r + 1r ~= 0";
 by (rtac (real_zero_less_two RS real_not_refl2 RS not_sym) 1);
 qed "real_two_not_zero";
-
 Addsimps [real_two_not_zero];
 
-Goal "x * inverse (1r + 1r) + x * inverse(1r + 1r) = x";
-by (stac real_add_self 1);
-by (full_simp_tac (simpset() addsimps [real_mult_assoc]) 1);
-qed "real_sum_of_halves";
-
 Goal "[| (0::real) < z; x < y |] ==> x*z < y*z";       
 by (rotate_tac 1 1);
 by (dtac real_less_sum_gt_zero 1);
 by (rtac real_sum_gt_zero_less 1);
 by (dtac real_mult_order 1 THEN assume_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [real_add_mult_distrib2,
-					   real_mult_commute ]) 1);
+by (asm_full_simp_tac
+    (simpset() addsimps [real_add_mult_distrib2, real_mult_commute ]) 1);
 qed "real_mult_less_mono1";
 
 Goal "[| (0::real) < z; x < y |] ==> z * x < z * y";       
-by (asm_simp_tac (simpset() addsimps [real_mult_commute,real_mult_less_mono1]) 1);
+by (asm_simp_tac
+    (simpset() addsimps [real_mult_commute,real_mult_less_mono1]) 1);
 qed "real_mult_less_mono2";
 
 Goal "[| (0::real) < z; x * z < y * z |] ==> x < y";
-by (forw_inst_tac [("x","x*z")] (real_inverse_gt_zero 
-                       RS real_mult_less_mono1) 1);
+by (forw_inst_tac [("x","x*z")] 
+    (real_inverse_gt_zero RS real_mult_less_mono1) 1);
 by (auto_tac (claset(),
-	      simpset() addsimps 
-     [real_mult_assoc,real_not_refl2 RS not_sym]));
+	      simpset() addsimps [real_mult_assoc,real_not_refl2 RS not_sym]));
 qed "real_mult_less_cancel1";
 
 Goal "[| (0::real) < z; z*x < z*y |] ==> x < y";
@@ -460,13 +453,13 @@
 qed "real_mult_less_cancel2";
 
 Goal "(0::real) < z ==> (x*z < y*z) = (x < y)";
-by (blast_tac (claset() addIs [real_mult_less_mono1,
-    real_mult_less_cancel1]) 1);
+by (blast_tac
+    (claset() addIs [real_mult_less_mono1, real_mult_less_cancel1]) 1);
 qed "real_mult_less_iff1";
 
 Goal "(0::real) < z ==> (z*x < z*y) = (x < y)";
-by (blast_tac (claset() addIs [real_mult_less_mono2,
-    real_mult_less_cancel2]) 1);
+by (blast_tac
+    (claset() addIs [real_mult_less_mono2, real_mult_less_cancel2]) 1);
 qed "real_mult_less_iff2";
 
 Addsimps [real_mult_less_iff1,real_mult_less_iff2];
@@ -484,7 +477,7 @@
 
 
 Goal "[| (0::real) <= z; x < y |] ==> x*z <= y*z";
-by (EVERY1 [rtac real_less_or_eq_imp_le, dtac real_le_imp_less_or_eq]);
+by (EVERY1 [rtac real_less_or_eq_imp_le, dtac order_le_imp_less_or_eq]);
 by (auto_tac (claset() addIs [real_mult_less_mono1],simpset()));
 qed "real_mult_le_less_mono1";
 
@@ -493,86 +486,68 @@
 qed "real_mult_le_less_mono2";
 
 Goal "[| (0::real) <= z; x <= y |] ==> z*x <= z*y";
-by (dres_inst_tac [("x","x")] real_le_imp_less_or_eq 1);
+by (dres_inst_tac [("x","x")] order_le_imp_less_or_eq 1);
 by (auto_tac (claset() addIs [real_mult_le_less_mono2], simpset()));
 qed "real_mult_le_le_mono1";
 
-Goal "[| (0::real) < r1; r1 < r2; 0 < x; x < y|] ==> r1 * x < r2 * y";
-by (dres_inst_tac [("x","x")] real_mult_less_mono2 1);
-by (dres_inst_tac [("R1.0","0")] real_less_trans 2);
-by (dres_inst_tac [("x","r1")] real_mult_less_mono1 3);
-by Auto_tac;
-by (blast_tac (claset() addIs [real_less_trans]) 1);
+Goal "[| u<v;  x<y;  (0::real) < v;  0 < x |] ==> u*x < v* y";
+by (etac (real_mult_less_mono1 RS order_less_trans) 1);
+by (assume_tac 1);
+by (etac real_mult_less_mono2 1);
+by (assume_tac 1);
 qed "real_mult_less_mono";
 
-Goal "[| (0::real) < r1; r1  < r2;  0 < y|] ==> 0 < r2 * y";
-by (rtac real_mult_order 1); 
-by (assume_tac 2);
-by (blast_tac (claset() addIs [real_less_trans]) 1);
-qed "real_mult_order_trans";
-
-Goal "[| (0::real) < r1; r1  < r2;  0 <= x; x < y|] ==> r1 * x < r2 * y";
-by (auto_tac (claset() addSDs [real_le_imp_less_or_eq] 
-	               addIs [real_mult_less_mono,real_mult_order_trans],
-              simpset()));
-qed "real_mult_less_mono3";
+Goal "[| x < y;  r1 < r2;  (0::real) <= r1;  0 <= x|] ==> r1 * x < r2 * y";
+by (subgoal_tac "0<r2" 1);
+by (blast_tac (claset() addIs [order_le_less_trans]) 2); 
+by (case_tac "x=0" 1);
+by (auto_tac (claset() addSDs [order_le_imp_less_or_eq] 
+	               addIs [real_mult_less_mono, real_mult_order],
+	      simpset()));
+qed "real_mult_less_mono'";
 
-Goal "[| (0::real) <= r1; r1  < r2;  0 <= x; x < y|] ==> r1 * x < r2 * y";
-by (auto_tac (claset() addSDs [real_le_imp_less_or_eq] 
-	               addIs [real_mult_less_mono,real_mult_order_trans,
-			      real_mult_order],
-	      simpset()));
-by (dres_inst_tac [("R2.0","x")] real_less_trans 1);
-by (assume_tac 1);
-by (blast_tac (claset() addIs [real_mult_order]) 1);
-qed "real_mult_less_mono4";
-
-Goal "[| (0::real) < r1; r1 <= r2;  0 <= x; x <= y |] ==> r1 * x <= r2 * y";
+Goal "[| r1 <= r2;  x <= y;  (0::real) < r1;  0 <= x |] ==> r1 * x <= r2 * y";
+by (subgoal_tac "0<r2" 1);
+by (blast_tac (claset() addIs [order_less_le_trans]) 2); 
 by (rtac real_less_or_eq_imp_le 1);
-by (REPEAT(dtac real_le_imp_less_or_eq 1));
-by (auto_tac (claset() addIs [real_mult_less_mono,
-			      real_mult_order_trans,real_mult_order],
+by (REPEAT(dtac order_le_imp_less_or_eq 1));
+by (auto_tac (claset() addIs [real_mult_less_mono, real_mult_order],
 	      simpset()));
 qed "real_mult_le_mono";
 
 Goal "[| (0::real) < r1; r1 < r2;  0 <= x; x <= y |] ==> r1 * x <= r2 * y";
-by (rtac real_less_or_eq_imp_le 1);
-by (REPEAT(dtac real_le_imp_less_or_eq 1));
-by (auto_tac (claset() addIs [real_mult_less_mono, real_mult_order_trans,
-			      real_mult_order],
-	      simpset()));
+by (blast_tac (claset() addIs [real_mult_le_mono, order_less_imp_le]) 1); 
 qed "real_mult_le_mono2";
 
 Goal "[| (0::real) <= r1; r1 < r2;  0 <= x; x <= y |] ==> r1 * x <= r2 * y";
-by (dtac real_le_imp_less_or_eq 1);
+by (dtac order_le_imp_less_or_eq 1);
 by (auto_tac (claset() addIs [real_mult_le_mono2],simpset()));
-by (dtac real_le_trans 1 THEN assume_tac 1);
+by (dtac order_trans 1 THEN assume_tac 1);
 by (auto_tac (claset() addIs [real_less_le_mult_order], simpset()));
 qed "real_mult_le_mono3";
 
 Goal "[| (0::real) <= r1; r1 <= r2;  0 <= x; x <= y |] ==> r1 * x <= r2 * y";
-by (dres_inst_tac [("x","r1")] real_le_imp_less_or_eq 1);
+by (dres_inst_tac [("x","r1")] order_le_imp_less_or_eq 1);
 by (auto_tac (claset() addIs [real_mult_le_mono3, real_mult_le_le_mono1],
 	      simpset()));
 qed "real_mult_le_mono4";
 
 Goal "1r <= x ==> 0 < x";
 by (rtac ccontr 1 THEN dtac real_leI 1);
-by (dtac real_le_trans 1 THEN assume_tac 1);
-by (auto_tac (claset() addDs [real_zero_less_one RSN (2,real_le_less_trans)],
-	      simpset() addsimps [real_less_not_refl]));
+by (dtac order_trans 1 THEN assume_tac 1);
+by (auto_tac (claset() addDs [real_zero_less_one RSN (2,order_le_less_trans)],
+	      simpset()));
 qed "real_gt_zero";
 
 Goal "[| 1r < r; 1r <= x |]  ==> x <= r * x";
-by (dtac (real_gt_zero RS real_less_imp_le) 1);
+by (dtac (real_gt_zero RS order_less_imp_le) 1);
 by (auto_tac (claset() addSDs [real_mult_le_less_mono1],
     simpset()));
 qed "real_mult_self_le";
 
 Goal "[| 1r <= r; 1r <= x |]  ==> x <= r * x";
-by (dtac real_le_imp_less_or_eq 1);
-by (auto_tac (claset() addIs [real_mult_self_le],
-	      simpset() addsimps [real_le_refl]));
+by (dtac order_le_imp_less_or_eq 1);
+by (auto_tac (claset() addIs [real_mult_self_le], simpset()));
 qed "real_mult_self_le2";
 
 Goal "(EX n. inverse (real_of_posnat n) < r) = (EX n. 1r < r * real_of_posnat n)";
@@ -599,9 +574,9 @@
 Goal "(inverse (real_of_posnat n) <= r) = (1r <= r * real_of_posnat n)";
 by (Step_tac 1);
 by (dres_inst_tac [("n2","n")] (real_of_posnat_gt_zero RS 
-    real_less_imp_le RS real_mult_le_le_mono1) 1);
+    order_less_imp_le RS real_mult_le_le_mono1) 1);
 by (dres_inst_tac [("n3","n")] (real_of_posnat_gt_zero RS 
-        real_inverse_gt_zero RS real_less_imp_le RS 
+        real_inverse_gt_zero RS order_less_imp_le RS 
         real_mult_le_le_mono1) 2);
 by (auto_tac (claset(), simpset() addsimps real_mult_ac));
 qed "real_of_posnat_inverse_le_iff";
@@ -636,7 +611,7 @@
 qed "real_of_posnat_inverse_eq_iff";
 
 Goal "[| 0 < r; r < x |] ==> inverse x < inverse (r::real)";
-by (ftac real_less_trans 1 THEN assume_tac 1);
+by (ftac order_less_trans 1 THEN assume_tac 1);
 by (ftac real_inverse_gt_zero 1);
 by (forw_inst_tac [("x","x")] real_inverse_gt_zero 1);
 by (forw_inst_tac [("x","r"),("z","inverse r")] real_mult_less_mono1 1);
@@ -657,7 +632,7 @@
 Addsimps [real_add_inverse_real_of_posnat_less];
 
 Goal "r <= r + inverse (real_of_posnat n)";
-by (rtac real_less_imp_le 1);
+by (rtac order_less_imp_le 1);
 by (Simp_tac 1);
 qed "real_add_inverse_real_of_posnat_le";
 Addsimps [real_add_inverse_real_of_posnat_le];
@@ -670,7 +645,7 @@
 Addsimps [real_add_minus_inverse_real_of_posnat_less];
 
 Goal "r + (-inverse (real_of_posnat n)) <= r";
-by (rtac real_less_imp_le 1);
+by (rtac order_less_imp_le 1);
 by (Simp_tac 1);
 qed "real_add_minus_inverse_real_of_posnat_le";
 Addsimps [real_add_minus_inverse_real_of_posnat_le];
diff -r a81ea5d3dd41 -r c4f1bf2acf4c src/HOL/Real/RealPow.ML
--- a/src/HOL/Real/RealPow.ML	Sat Dec 30 22:03:47 2000 +0100
+++ b/src/HOL/Real/RealPow.ML	Sat Dec 30 22:13:18 2000 +0100
@@ -29,8 +29,7 @@
 
 Goal "abs (r::real) ^ n = abs (r ^ n)";
 by (induct_tac "n" 1);
-by (auto_tac (claset(),simpset() addsimps 
-    [abs_mult,abs_one]));
+by (auto_tac (claset(), simpset() addsimps [abs_mult]));
 qed "realpow_abs";
 
 Goal "(r::real) ^ (n + m) = (r ^ n) * (r ^ m)";
@@ -49,7 +48,7 @@
 
 Goal "(#0::real) < r --> #0 <= r ^ n";
 by (induct_tac "n" 1);
-by (auto_tac (claset() addDs [real_less_imp_le] 
+by (auto_tac (claset() addDs [order_less_imp_le] 
 	               addIs [rename_numerals real_le_mult_order],
 	      simpset()));
 qed_spec_mp "realpow_ge_zero";
@@ -87,20 +86,15 @@
     simpset()));
 qed_spec_mp "realpow_less";
 
-Goal  "#1 ^ n = (#1::real)";
+Goal "#1 ^ n = (#1::real)";
 by (induct_tac "n" 1);
 by Auto_tac;
 qed "realpow_eq_one";
 Addsimps [realpow_eq_one];
 
-Goal "abs(-(#1 ^ n)) = (#1::real)";
-by (simp_tac (simpset() addsimps [abs_one]) 1);
-qed "abs_minus_realpow_one";
-Addsimps [abs_minus_realpow_one];
-
 Goal "abs((#-1) ^ n) = (#1::real)";
 by (induct_tac "n" 1);
-by (auto_tac (claset(),simpset() addsimps [abs_mult,abs_one]));
+by (auto_tac (claset(), simpset() addsimps [abs_mult]));
 qed "abs_realpow_minus_one";
 Addsimps [abs_realpow_minus_one];
 
@@ -129,59 +123,30 @@
 Goal "(#1::real) < r ==> #1 < r^2";
 by Auto_tac;
 by (cut_facts_tac [rename_numerals real_zero_less_one] 1);
-by (forw_inst_tac [("R1.0","#0")] real_less_trans 1);
+by (forw_inst_tac [("x","#0")] order_less_trans 1);
 by (assume_tac 1);
 by (dres_inst_tac [("z","r"),("x","#1")] 
     (rename_numerals real_mult_less_mono1) 1);
-by (auto_tac (claset() addIs [real_less_trans],simpset()));
+by (auto_tac (claset() addIs [order_less_trans], simpset()));
 qed "realpow_two_gt_one";
 
 Goal "(#1::real) < r --> #1 <= r ^ n";
 by (induct_tac "n" 1);
-by (auto_tac (claset() addSDs [real_le_imp_less_or_eq],
-	      simpset()));
-by (dtac (rename_numerals (real_zero_less_one RS real_mult_less_mono)) 1);
-by (auto_tac (claset() addSIs [real_less_imp_le],
-	      simpset() addsimps [real_zero_less_one]));
+by Auto_tac;  
+by (subgoal_tac "#1*#1 <= r * r^n" 1);
+by (rtac real_mult_le_mono 2); 
+by Auto_tac;  
 qed_spec_mp "realpow_ge_one";
 
-Goal "(#1::real) < r ==> #1 < r ^ (Suc n)";
-by (forw_inst_tac [("n","n")] realpow_ge_one 1);
-by (dtac real_le_imp_less_or_eq 1 THEN Step_tac 1);
-by (dtac sym 2);
-by (ftac (rename_numerals (real_zero_less_one RS real_less_trans)) 1);
-by (dres_inst_tac [("y","r ^ n")] 
-    (rename_numerals real_mult_less_mono2) 1);
-by (assume_tac 1);
-by (auto_tac (claset() addDs [real_less_trans],
-     simpset()));
-qed "realpow_Suc_gt_one";
-
 Goal "(#1::real) <= r ==> #1 <= r ^ n";
-by (dtac real_le_imp_less_or_eq 1); 
+by (dtac order_le_imp_less_or_eq 1); 
 by (auto_tac (claset() addDs [realpow_ge_one], simpset()));
 qed "realpow_ge_one2";
 
-Goal "(#0::real) < r ==> #0 < r ^ Suc n";
-by (forw_inst_tac [("n","n")] realpow_ge_zero 1);
-by (forw_inst_tac [("n1","n")]
-    ((real_not_refl2 RS not_sym) RS realpow_not_zero RS not_sym) 1);
-by (auto_tac (claset() addSDs [real_le_imp_less_or_eq]
-                       addIs [rename_numerals real_mult_order],
-              simpset()));
-qed "realpow_Suc_gt_zero";
-
-Goal "(#0::real) <= r ==> #0 <= r ^ Suc n";
-by (etac (real_le_imp_less_or_eq RS disjE) 1);
-by (etac (realpow_ge_zero) 1);
-by (dtac sym 1);
-by (Asm_simp_tac 1);
-qed "realpow_Suc_ge_zero";
-
 Goal "(#1::real) <= #2 ^ n";
-by (res_inst_tac [("j","#1 ^ n")] real_le_trans 1);
+by (res_inst_tac [("y","#1 ^ n")] order_trans 1);
 by (rtac realpow_le 2);
-by (auto_tac (claset() addIs [real_less_imp_le],simpset()));
+by (auto_tac (claset() addIs [order_less_imp_le],simpset()));
 qed "two_realpow_ge_one";
 
 Goal "real_of_nat n < #2 ^ n";
@@ -217,8 +182,9 @@
 
 Goal "#0 <= r & r < (#1::real) --> r ^ Suc n <= r ^ n";
 by (induct_tac "n" 1);
-by (auto_tac (claset() addIs [real_less_imp_le] addSDs
-     [real_le_imp_less_or_eq],simpset()));
+by (auto_tac (claset() addIs [order_less_imp_le] 
+                       addSDs [order_le_imp_less_or_eq],
+              simpset()));
 qed_spec_mp "realpow_Suc_le";
 
 Goal "(#0::real) <= #0 ^ n";
@@ -228,12 +194,12 @@
 Addsimps [realpow_zero_le];
 
 Goal "#0 < r & r < (#1::real) --> r ^ Suc n <= r ^ n";
-by (blast_tac (claset() addSIs [real_less_imp_le,
+by (blast_tac (claset() addSIs [order_less_imp_le,
     realpow_Suc_less]) 1);
 qed_spec_mp "realpow_Suc_le2";
 
 Goal "[| #0 <= r; r < (#1::real) |] ==> r ^ Suc n <= r ^ n";
-by (etac (real_le_imp_less_or_eq RS disjE) 1);
+by (etac (order_le_imp_less_or_eq RS disjE) 1);
 by (rtac realpow_Suc_le2 1);
 by Auto_tac;
 qed "realpow_Suc_le3";
@@ -257,13 +223,12 @@
 
 Goal "[| #0 < r; r < (#1::real) |] ==> r ^ Suc n <= r";
 by (dres_inst_tac [("n","1"),("N","Suc n")] 
-    (real_less_imp_le RS realpow_le_le) 1);
+    (order_less_imp_le RS realpow_le_le) 1);
 by Auto_tac;
 qed "realpow_Suc_le_self";
 
 Goal "[| #0 < r; r < (#1::real) |] ==> r ^ Suc n < #1";
-by (blast_tac (claset() addIs [realpow_Suc_le_self,
-               real_le_less_trans]) 1);
+by (blast_tac (claset() addIs [realpow_Suc_le_self, order_le_less_trans]) 1);
 qed "realpow_Suc_less_one";
 
 Goal "(#1::real) <= r --> r ^ n <= r ^ Suc n";
@@ -277,8 +242,7 @@
 qed_spec_mp "realpow_less_Suc";
 
 Goal "(#1::real) < r --> r ^ n <= r ^ Suc n";
-by (blast_tac (claset() addSIs [real_less_imp_le,
-    realpow_less_Suc]) 1);
+by (blast_tac (claset() addSIs [order_less_imp_le, realpow_less_Suc]) 1);
 qed_spec_mp "realpow_le_Suc2";
 
 Goal "(#1::real) < r & n < N --> r ^ n <= r ^ N";
@@ -288,8 +252,8 @@
 by (ALLGOALS(dtac (rename_numerals real_mult_self_le)));
 by (assume_tac 1);
 by (assume_tac 2);
-by (auto_tac (claset() addIs [real_le_trans],
-    simpset() addsimps [less_Suc_eq]));
+by (auto_tac (claset() addIs [order_trans],
+              simpset() addsimps [less_Suc_eq]));
 qed_spec_mp "realpow_gt_ge";
 
 Goal "(#1::real) <= r & n < N --> r ^ n <= r ^ N";
@@ -299,18 +263,18 @@
 by (ALLGOALS(dtac (rename_numerals real_mult_self_le2)));
 by (assume_tac 1);
 by (assume_tac 2);
-by (auto_tac (claset() addIs [real_le_trans],
-    simpset() addsimps [less_Suc_eq]));
+by (auto_tac (claset() addIs [order_trans],
+              simpset() addsimps [less_Suc_eq]));
 qed_spec_mp "realpow_gt_ge2";
 
 Goal "[| (#1::real) < r; n <= N |] ==> r ^ n <= r ^ N";
 by (dres_inst_tac [("n","N")] le_imp_less_or_eq 1);
-by (auto_tac (claset() addIs [realpow_gt_ge],simpset()));
+by (auto_tac (claset() addIs [realpow_gt_ge], simpset()));
 qed "realpow_ge_ge";
 
 Goal "[| (#1::real) <= r; n <= N |] ==> r ^ n <= r ^ N";
 by (dres_inst_tac [("n","N")] le_imp_less_or_eq 1);
-by (auto_tac (claset() addIs [realpow_gt_ge2],simpset()));
+by (auto_tac (claset() addIs [realpow_gt_ge2], simpset()));
 qed "realpow_ge_ge2";
 
 Goal "(#1::real) < r ==> r <= r ^ Suc n";
@@ -390,17 +354,13 @@
 Goal "(#0::real) <= x --> #0 <= y --> x ^ Suc n <= y ^ Suc n --> x <= y";
 by (induct_tac "n" 1);
 by Auto_tac;
-by (rtac real_leI 1);
-by (auto_tac (claset(), 
-              simpset() addsimps [inst "x" "#0" order_le_less,
-                                  real_mult_le_0_iff])); 
-by (subgoal_tac "inverse x * (x * (x * x ^ n)) <= inverse y * (y * (y * y ^ n))" 1);
-by (rtac real_mult_le_mono 2);
-by (asm_full_simp_tac (simpset() addsimps [realpow_ge_zero, real_0_le_mult_iff]) 4); 
-by (asm_full_simp_tac (simpset() addsimps [real_inverse_le_iff]) 3);
-by (asm_full_simp_tac (simpset() addsimps [real_mult_assoc RS sym]) 1);
-by (rtac real_inverse_gt_zero 1);  
-by Auto_tac; 
+by (asm_full_simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1); 
+by (swap_res_tac [real_mult_less_mono'] 1);
+by Auto_tac;
+by (auto_tac (claset(), simpset() addsimps [real_0_le_mult_iff]));
+by (auto_tac (claset(), simpset() addsimps [linorder_not_less RS sym]));    
+by (dres_inst_tac [("n","n")] realpow_gt_zero 1);   
+by Auto_tac;  
 qed_spec_mp "realpow_increasing";
   
 Goal "[| (#0::real) <= x; #0 <= y; x ^ Suc n = y ^ Suc n |] ==> x = y";