# HG changeset patch
# User paulson
# Date 1052235954 -7200
# Node ID 2160abf7cfe73ab8d04cfbd054b6a18758b334fe
# Parent  46ad7fd03a38fc480d97830469de630adf01a864
removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex

diff -r 46ad7fd03a38 -r 2160abf7cfe7 NEWS
--- a/NEWS	Tue May 06 12:29:49 2003 +0200
+++ b/NEWS	Tue May 06 17:45:54 2003 +0200
@@ -152,11 +152,16 @@
 implicit structures.  Also a new, experimental summation operator for
 abelian groups;
 
-* Complex: new directory of the complex numbers with numeric constants, nonstandard complex numbers, and some complex analysis, standard and nonstandard (Jacques Fleuriot);
-
 * GroupTheory: deleted, since its material has been moved to Algebra;
 
-* Hyperreal: introduced Gauge integration and hyperreal logarithms (Jacques Fleuriot);
+* Complex: new directory of the complex numbers with numeric constants, 
+nonstandard complex numbers, and some complex analysis, standard and 
+nonstandard (Jacques Fleuriot);
+
+* HOL-Complex: new image for analysis, replacing HOL-Real and HOL-Hyperreal;
+
+* Hyperreal: introduced Gauge integration and hyperreal logarithms (Jacques 
+Fleuriot);
 
 * Real/HahnBanach: updated and adapted to locales;
 
diff -r 46ad7fd03a38 -r 2160abf7cfe7 src/HOL/Complex/ROOT.ML
--- a/src/HOL/Complex/ROOT.ML	Tue May 06 12:29:49 2003 +0200
+++ b/src/HOL/Complex/ROOT.ML	Tue May 06 17:45:54 2003 +0200
@@ -5,5 +5,7 @@
 The Complex Numbers
 *)
 
+no_document time_use_thy "Ring_and_Field";
+with_path "../Real" use_thy "Real";
 with_path "../Hyperreal" use_thy "Hyperreal";
 time_use_thy "CLim";
diff -r 46ad7fd03a38 -r 2160abf7cfe7 src/HOL/Complex/ex/BinEx.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Complex/ex/BinEx.thy	Tue May 06 17:45:54 2003 +0200
@@ -0,0 +1,370 @@
+(*  Title:      HOL/Real/ex/BinEx.thy
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1999  University of Cambridge
+*)
+
+header {* Binary arithmetic examples *}
+
+theory BinEx = Real:
+
+text {*
+  Examples of performing binary arithmetic by simplification This time
+  we use the reals, though the representation is just of integers.
+*}
+
+text {* \medskip Addition *}
+
+lemma "(1359::real) + -2468 = -1109"
+  by simp
+
+lemma "(93746::real) + -46375 = 47371"
+  by simp
+
+
+text {* \medskip Negation *}
+
+lemma "- (65745::real) = -65745"
+  by simp
+
+lemma "- (-54321::real) = 54321"
+  by simp
+
+
+text {* \medskip Multiplication *}
+
+lemma "(-84::real) * 51 = -4284"
+  by simp
+
+lemma "(255::real) * 255 = 65025"
+  by simp
+
+lemma "(1359::real) * -2468 = -3354012"
+  by simp
+
+
+text {* \medskip Inequalities *}
+
+lemma "(89::real) * 10 \<noteq> 889"
+  by simp
+
+lemma "(13::real) < 18 - 4"
+  by simp
+
+lemma "(-345::real) < -242 + -100"
+  by simp
+
+lemma "(13557456::real) < 18678654"
+  by simp
+
+lemma "(999999::real) \<le> (1000001 + 1) - 2"
+  by simp
+
+lemma "(1234567::real) \<le> 1234567"
+  by simp
+
+
+text {* \medskip Powers *}
+
+lemma "2 ^ 15 = (32768::real)"
+  by simp
+
+lemma "-3 ^ 7 = (-2187::real)"
+  by simp
+
+lemma "13 ^ 7 = (62748517::real)"
+  by simp
+
+lemma "3 ^ 15 = (14348907::real)"
+  by simp
+
+lemma "-5 ^ 11 = (-48828125::real)"
+  by simp
+
+
+text {* \medskip Tests *}
+
+lemma "(x + y = x) = (y = (0::real))"
+  by arith
+
+lemma "(x + y = y) = (x = (0::real))"
+  by arith
+
+lemma "(x + y = (0::real)) = (x = -y)"
+  by arith
+
+lemma "(x + y = (0::real)) = (y = -x)"
+  by arith
+
+lemma "((x + y) < (x + z)) = (y < (z::real))"
+  by arith
+
+lemma "((x + z) < (y + z)) = (x < (y::real))"
+  by arith
+
+lemma "(\<not> x < y) = (y \<le> (x::real))"
+  by arith
+
+lemma "\<not> (x < y \<and> y < (x::real))"
+  by arith
+
+lemma "(x::real) < y ==> \<not> y < x"
+  by arith
+
+lemma "((x::real) \<noteq> y) = (x < y \<or> y < x)"
+  by arith
+
+lemma "(\<not> x \<le> y) = (y < (x::real))"
+  by arith
+
+lemma "x \<le> y \<or> y \<le> (x::real)"
+  by arith
+
+lemma "x \<le> y \<or> y < (x::real)"
+  by arith
+
+lemma "x < y \<or> y \<le> (x::real)"
+  by arith
+
+lemma "x \<le> (x::real)"
+  by arith
+
+lemma "((x::real) \<le> y) = (x < y \<or> x = y)"
+  by arith
+
+lemma "((x::real) \<le> y \<and> y \<le> x) = (x = y)"
+  by arith
+
+lemma "\<not>(x < y \<and> y \<le> (x::real))"
+  by arith
+
+lemma "\<not>(x \<le> y \<and> y < (x::real))"
+  by arith
+
+lemma "(-x < (0::real)) = (0 < x)"
+  by arith
+
+lemma "((0::real) < -x) = (x < 0)"
+  by arith
+
+lemma "(-x \<le> (0::real)) = (0 \<le> x)"
+  by arith
+
+lemma "((0::real) \<le> -x) = (x \<le> 0)"
+  by arith
+
+lemma "(x::real) = y \<or> x < y \<or> y < x"
+  by arith
+
+lemma "(x::real) = 0 \<or> 0 < x \<or> 0 < -x"
+  by arith
+
+lemma "(0::real) \<le> x \<or> 0 \<le> -x"
+  by arith
+
+lemma "((x::real) + y \<le> x + z) = (y \<le> z)"
+  by arith
+
+lemma "((x::real) + z \<le> y + z) = (x \<le> y)"
+  by arith
+
+lemma "(w::real) < x \<and> y < z ==> w + y < x + z"
+  by arith
+
+lemma "(w::real) \<le> x \<and> y \<le> z ==> w + y \<le> x + z"
+  by arith
+
+lemma "(0::real) \<le> x \<and> 0 \<le> y ==> 0 \<le> x + y"
+  by arith
+
+lemma "(0::real) < x \<and> 0 < y ==> 0 < x + y"
+  by arith
+
+lemma "(-x < y) = (0 < x + (y::real))"
+  by arith
+
+lemma "(x < -y) = (x + y < (0::real))"
+  by arith
+
+lemma "(y < x + -z) = (y + z < (x::real))"
+  by arith
+
+lemma "(x + -y < z) = (x < z + (y::real))"
+  by arith
+
+lemma "x \<le> y ==> x < y + (1::real)"
+  by arith
+
+lemma "(x - y) + y = (x::real)"
+  by arith
+
+lemma "y + (x - y) = (x::real)"
+  by arith
+
+lemma "x - x = (0::real)"
+  by arith
+
+lemma "(x - y = 0) = (x = (y::real))"
+  by arith
+
+lemma "((0::real) \<le> x + x) = (0 \<le> x)"
+  by arith
+
+lemma "(-x \<le> x) = ((0::real) \<le> x)"
+  by arith
+
+lemma "(x \<le> -x) = (x \<le> (0::real))"
+  by arith
+
+lemma "(-x = (0::real)) = (x = 0)"
+  by arith
+
+lemma "-(x - y) = y - (x::real)"
+  by arith
+
+lemma "((0::real) < x - y) = (y < x)"
+  by arith
+
+lemma "((0::real) \<le> x - y) = (y \<le> x)"
+  by arith
+
+lemma "(x + y) - x = (y::real)"
+  by arith
+
+lemma "(-x = y) = (x = (-y::real))"
+  by arith
+
+lemma "x < (y::real) ==> \<not>(x = y)"
+  by arith
+
+lemma "(x \<le> x + y) = ((0::real) \<le> y)"
+  by arith
+
+lemma "(y \<le> x + y) = ((0::real) \<le> x)"
+  by arith
+
+lemma "(x < x + y) = ((0::real) < y)"
+  by arith
+
+lemma "(y < x + y) = ((0::real) < x)"
+  by arith
+
+lemma "(x - y) - x = (-y::real)"
+  by arith
+
+lemma "(x + y < z) = (x < z - (y::real))"
+  by arith
+
+lemma "(x - y < z) = (x < z + (y::real))"
+  by arith
+
+lemma "(x < y - z) = (x + z < (y::real))"
+  by arith
+
+lemma "(x \<le> y - z) = (x + z \<le> (y::real))"
+  by arith
+
+lemma "(x - y \<le> z) = (x \<le> z + (y::real))"
+  by arith
+
+lemma "(-x < -y) = (y < (x::real))"
+  by arith
+
+lemma "(-x \<le> -y) = (y \<le> (x::real))"
+  by arith
+
+lemma "(a + b) - (c + d) = (a - c) + (b - (d::real))"
+  by arith
+
+lemma "(0::real) - x = -x"
+  by arith
+
+lemma "x - (0::real) = x"
+  by arith
+
+lemma "w \<le> x \<and> y < z ==> w + y < x + (z::real)"
+  by arith
+
+lemma "w < x \<and> y \<le> z ==> w + y < x + (z::real)"
+  by arith
+
+lemma "(0::real) \<le> x \<and> 0 < y ==> 0 < x + (y::real)"
+  by arith
+
+lemma "(0::real) < x \<and> 0 \<le> y ==> 0 < x + y"
+  by arith
+
+lemma "-x - y = -(x + (y::real))"
+  by arith
+
+lemma "x - (-y) = x + (y::real)"
+  by arith
+
+lemma "-x - -y = y - (x::real)"
+  by arith
+
+lemma "(a - b) + (b - c) = a - (c::real)"
+  by arith
+
+lemma "(x = y - z) = (x + z = (y::real))"
+  by arith
+
+lemma "(x - y = z) = (x = z + (y::real))"
+  by arith
+
+lemma "x - (x - y) = (y::real)"
+  by arith
+
+lemma "x - (x + y) = -(y::real)"
+  by arith
+
+lemma "x = y ==> x \<le> (y::real)"
+  by arith
+
+lemma "(0::real) < x ==> \<not>(x = 0)"
+  by arith
+
+lemma "(x + y) * (x - y) = (x * x) - (y * y)"
+  oops
+
+lemma "(-x = -y) = (x = (y::real))"
+  by arith
+
+lemma "(-x < -y) = (y < (x::real))"
+  by arith
+
+lemma "!!a::real. a \<le> b ==> c \<le> d ==> x + y < z ==> a + c \<le> b + d"
+  by (tactic "fast_arith_tac 1")
+
+lemma "!!a::real. a < b ==> c < d ==> a - d \<le> b + (-c)"
+  by (tactic "fast_arith_tac 1")
+
+lemma "!!a::real. a \<le> b ==> b + b \<le> c ==> a + a \<le> c"
+  by (tactic "fast_arith_tac 1")
+
+lemma "!!a::real. a + b \<le> i + j ==> a \<le> b ==> i \<le> j ==> a + a \<le> j + j"
+  by (tactic "fast_arith_tac 1")
+
+lemma "!!a::real. a + b < i + j ==> a < b ==> i < j ==> a + a < j + j"
+  by (tactic "fast_arith_tac 1")
+
+lemma "!!a::real. a + b + c \<le> i + j + k \<and> a \<le> b \<and> b \<le> c \<and> i \<le> j \<and> j \<le> k --> a + a + a \<le> k + k + k"
+  by arith
+
+lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c
+    ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a \<le> l"
+  by (tactic "fast_arith_tac 1")
+
+lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c
+    ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a + a + a + a \<le> l + l + l + l"
+  by (tactic "fast_arith_tac 1")
+
+lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c
+    ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a + a + a + a + a \<le> l + l + l + l + i"
+  by (tactic "fast_arith_tac 1")
+
+lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c
+    ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a + a + a + a + a + a \<le> l + l + l + l + i + l"
+  by (tactic "fast_arith_tac 1")
+
+end
diff -r 46ad7fd03a38 -r 2160abf7cfe7 src/HOL/Complex/ex/ROOT.ML
--- a/src/HOL/Complex/ex/ROOT.ML	Tue May 06 12:29:49 2003 +0200
+++ b/src/HOL/Complex/ex/ROOT.ML	Tue May 06 17:45:54 2003 +0200
@@ -1,9 +1,10 @@
-(*  Title:      HOL/Hyperreal/ex/ROOT.ML
+(*  Title:      HOL/Complex/ex/ROOT.ML
     ID:         $Id$
 
-Miscellaneous HOL-Hyperreal Examples.
+Miscellaneous examples involving the Reals, Hyperreals, etc.
 *)
 
+use_thy "BinEx";
 no_document (with_path "../../NumberTheory" use_thy) "Factorization";
 (*These two examples just need the theory Primes.*)
 use_thy "Sqrt";
diff -r 46ad7fd03a38 -r 2160abf7cfe7 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue May 06 12:29:49 2003 +0200
+++ b/src/HOL/IsaMakefile	Tue May 06 17:45:54 2003 +0200
@@ -7,7 +7,7 @@
 ## targets
 
 default: HOL
-images: HOL HOL-Algebra HOL-Real HOL-Complex TLA
+images: HOL HOL-Algebra HOL-Complex TLA
 
 #Note: keep targets sorted (except for HOL-Library)
 test: \
@@ -19,7 +19,6 @@
   HOL-CTL \
   HOL-Extraction \
       HOL-Real-HahnBanach \
-      HOL-Real-ex \
   HOL-Hoare \
   HOL-HoareParallel \
   HOL-IMP \
@@ -113,35 +112,10 @@
 	@$(ISATOOL) usedir -b -g true $(OUT)/Pure HOL
 
 
-## HOL-Real
-
-HOL-Real: HOL $(OUT)/HOL-Real
-
-$(OUT)/HOL-Real: $(OUT)/HOL Real/Complex_Numbers.thy \
-  Real/Lubs.ML Real/Lubs.thy Real/PNat.ML Real/PNat.thy \
-  Real/PRat.ML Real/PRat.thy \
-  Real/PReal.ML Real/PReal.thy Real/RComplete.ML Real/RComplete.thy \
-  Real/ROOT.ML Real/Real.thy Real/RealAbs.ML Real/RealAbs.thy \
-  Real/RealArith0.ML Real/RealArith0.thy Real/real_arith0.ML \
-  Real/RealArith.thy Real/real_arith.ML Real/RealBin.ML \
-  Real/RealBin.thy Real/RealDef.ML Real/RealDef.thy Real/RealInt.ML \
-  Real/RealInt.thy Real/RealOrd.ML Real/RealOrd.thy Real/RealPow.ML \
-  Real/RealPow.thy Real/document/root.tex Real/real_arith.ML
-	@cd Real; $(ISATOOL) usedir -b $(OUT)/HOL HOL-Real
-
-
-## HOL-Real-ex
-
-HOL-Real-ex: HOL-Real $(LOG)/HOL-Real-ex.gz
-
-$(LOG)/HOL-Real-ex.gz: $(OUT)/HOL-Real Real/ex/ROOT.ML \
-  Real/ex/BinEx.thy Real/ex/document/root.tex
-	@cd Real; $(ISATOOL) usedir $(OUT)/HOL-Real ex
-
 
 ## HOL-Real-HahnBanach
 
-HOL-Real-HahnBanach: HOL-Real $(LOG)/HOL-Real-HahnBanach.gz
+HOL-Real-HahnBanach: HOL-Complex $(LOG)/HOL-Real-HahnBanach.gz
 
 $(LOG)/HOL-Real-HahnBanach.gz: $(OUT)/HOL-Real Real/HahnBanach/Aux.thy \
   Real/HahnBanach/Bounds.thy Real/HahnBanach/FunctionNorm.thy \
@@ -153,15 +127,25 @@
   Real/HahnBanach/Subspace.thy Real/HahnBanach/VectorSpace.thy \
   Real/HahnBanach/ZornLemma.thy Real/HahnBanach/document/root.bib \
   Real/HahnBanach/document/root.tex
-	@cd Real; $(ISATOOL) usedir -g true $(OUT)/HOL-Real HahnBanach
+	@cd Real; $(ISATOOL) usedir -g true $(OUT)/HOL-Complex HahnBanach
 
 
 ## HOL-Complex
 
-HOL-Complex: HOL-Real $(OUT)/HOL-Complex
+HOL-Complex: HOL $(OUT)/HOL-Complex
 
-$(OUT)/HOL-Complex: $(OUT)/HOL-Real Complex/ROOT.ML\
+$(OUT)/HOL-Complex: $(OUT)/HOL Complex/ROOT.ML\
   Library/Zorn.thy\
+  Real/Complex_Numbers.thy \
+  Real/Lubs.ML Real/Lubs.thy Real/PNat.ML Real/PNat.thy \
+  Real/PRat.ML Real/PRat.thy \
+  Real/PReal.ML Real/PReal.thy Real/RComplete.ML Real/RComplete.thy \
+  Real/ROOT.ML Real/Real.thy Real/RealAbs.ML Real/RealAbs.thy \
+  Real/RealArith0.ML Real/RealArith0.thy Real/real_arith0.ML \
+  Real/RealArith.thy Real/real_arith.ML Real/RealBin.ML \
+  Real/RealBin.thy Real/RealDef.ML Real/RealDef.thy Real/RealInt.ML \
+  Real/RealInt.thy Real/RealOrd.ML Real/RealOrd.thy Real/RealPow.ML \
+  Real/RealPow.thy Real/document/root.tex Real/real_arith.ML\
   Hyperreal/EvenOdd.ML Hyperreal/EvenOdd.thy Hyperreal/ExtraThms2.ML\
   Hyperreal/ExtraThms2.thy Hyperreal/Fact.ML Hyperreal/Fact.thy\
   Hyperreal/Filter.ML Hyperreal/Filter.thy Hyperreal/HRealAbs.ML\
@@ -191,7 +175,7 @@
   Complex/NSComplex.ML Complex/NSComplex.thy\
   Complex/NSComplexArith0.ML Complex/NSComplexArith0.thy\
   Complex/NSComplexBin.ML Complex/NSComplexBin.thy
-	@cd Complex; $(ISATOOL) usedir -b $(OUT)/HOL-Real HOL-Complex
+	@cd Complex; $(ISATOOL) usedir -b $(OUT)/HOL HOL-Complex
 
 
 ## HOL-Complex-ex
@@ -200,6 +184,7 @@
 
 $(LOG)/HOL-Complex-ex.gz: $(OUT)/HOL-Complex Library/Primes.thy \
   Complex/ex/ROOT.ML Complex/ex/document/root.tex \
+  Complex/ex/BinEx.thy \
   Complex/ex/NSPrimes.ML Complex/ex/NSPrimes.thy\
   Complex/ex/Sqrt.thy Complex/ex/Sqrt_Script.thy
 	@cd Complex; $(ISATOOL) usedir $(OUT)/HOL-Complex ex
@@ -675,7 +660,7 @@
 ## clean
 
 clean:
-	@rm -f  $(OUT)/HOL $(OUT)/HOL-Real $(OUT)/HOL-Complex $(OUT)/TLA \
+	@rm -f  $(OUT)/HOL $(OUT)/HOL-Complex $(OUT)/TLA \
 		$(LOG)/HOL.gz $(LOG)/HOL-Real.gz $(LOG)/TLA.gz \
 		$(LOG)/HOL-Isar_examples.gz $(LOG)/HOL-Induct.gz \
 		$(LOG)/HOL-ex.gz $(LOG)/HOL-Subst.gz $(LOG)/HOL-IMP.gz \
diff -r 46ad7fd03a38 -r 2160abf7cfe7 src/HOL/Real/ex/BinEx.thy
--- a/src/HOL/Real/ex/BinEx.thy	Tue May 06 12:29:49 2003 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,370 +0,0 @@
-(*  Title:      HOL/Real/ex/BinEx.thy
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1999  University of Cambridge
-*)
-
-header {* Binary arithmetic examples *}
-
-theory BinEx = Real:
-
-text {*
-  Examples of performing binary arithmetic by simplification This time
-  we use the reals, though the representation is just of integers.
-*}
-
-text {* \medskip Addition *}
-
-lemma "(1359::real) + -2468 = -1109"
-  by simp
-
-lemma "(93746::real) + -46375 = 47371"
-  by simp
-
-
-text {* \medskip Negation *}
-
-lemma "- (65745::real) = -65745"
-  by simp
-
-lemma "- (-54321::real) = 54321"
-  by simp
-
-
-text {* \medskip Multiplication *}
-
-lemma "(-84::real) * 51 = -4284"
-  by simp
-
-lemma "(255::real) * 255 = 65025"
-  by simp
-
-lemma "(1359::real) * -2468 = -3354012"
-  by simp
-
-
-text {* \medskip Inequalities *}
-
-lemma "(89::real) * 10 \<noteq> 889"
-  by simp
-
-lemma "(13::real) < 18 - 4"
-  by simp
-
-lemma "(-345::real) < -242 + -100"
-  by simp
-
-lemma "(13557456::real) < 18678654"
-  by simp
-
-lemma "(999999::real) \<le> (1000001 + 1) - 2"
-  by simp
-
-lemma "(1234567::real) \<le> 1234567"
-  by simp
-
-
-text {* \medskip Powers *}
-
-lemma "2 ^ 15 = (32768::real)"
-  by simp
-
-lemma "-3 ^ 7 = (-2187::real)"
-  by simp
-
-lemma "13 ^ 7 = (62748517::real)"
-  by simp
-
-lemma "3 ^ 15 = (14348907::real)"
-  by simp
-
-lemma "-5 ^ 11 = (-48828125::real)"
-  by simp
-
-
-text {* \medskip Tests *}
-
-lemma "(x + y = x) = (y = (0::real))"
-  by arith
-
-lemma "(x + y = y) = (x = (0::real))"
-  by arith
-
-lemma "(x + y = (0::real)) = (x = -y)"
-  by arith
-
-lemma "(x + y = (0::real)) = (y = -x)"
-  by arith
-
-lemma "((x + y) < (x + z)) = (y < (z::real))"
-  by arith
-
-lemma "((x + z) < (y + z)) = (x < (y::real))"
-  by arith
-
-lemma "(\<not> x < y) = (y \<le> (x::real))"
-  by arith
-
-lemma "\<not> (x < y \<and> y < (x::real))"
-  by arith
-
-lemma "(x::real) < y ==> \<not> y < x"
-  by arith
-
-lemma "((x::real) \<noteq> y) = (x < y \<or> y < x)"
-  by arith
-
-lemma "(\<not> x \<le> y) = (y < (x::real))"
-  by arith
-
-lemma "x \<le> y \<or> y \<le> (x::real)"
-  by arith
-
-lemma "x \<le> y \<or> y < (x::real)"
-  by arith
-
-lemma "x < y \<or> y \<le> (x::real)"
-  by arith
-
-lemma "x \<le> (x::real)"
-  by arith
-
-lemma "((x::real) \<le> y) = (x < y \<or> x = y)"
-  by arith
-
-lemma "((x::real) \<le> y \<and> y \<le> x) = (x = y)"
-  by arith
-
-lemma "\<not>(x < y \<and> y \<le> (x::real))"
-  by arith
-
-lemma "\<not>(x \<le> y \<and> y < (x::real))"
-  by arith
-
-lemma "(-x < (0::real)) = (0 < x)"
-  by arith
-
-lemma "((0::real) < -x) = (x < 0)"
-  by arith
-
-lemma "(-x \<le> (0::real)) = (0 \<le> x)"
-  by arith
-
-lemma "((0::real) \<le> -x) = (x \<le> 0)"
-  by arith
-
-lemma "(x::real) = y \<or> x < y \<or> y < x"
-  by arith
-
-lemma "(x::real) = 0 \<or> 0 < x \<or> 0 < -x"
-  by arith
-
-lemma "(0::real) \<le> x \<or> 0 \<le> -x"
-  by arith
-
-lemma "((x::real) + y \<le> x + z) = (y \<le> z)"
-  by arith
-
-lemma "((x::real) + z \<le> y + z) = (x \<le> y)"
-  by arith
-
-lemma "(w::real) < x \<and> y < z ==> w + y < x + z"
-  by arith
-
-lemma "(w::real) \<le> x \<and> y \<le> z ==> w + y \<le> x + z"
-  by arith
-
-lemma "(0::real) \<le> x \<and> 0 \<le> y ==> 0 \<le> x + y"
-  by arith
-
-lemma "(0::real) < x \<and> 0 < y ==> 0 < x + y"
-  by arith
-
-lemma "(-x < y) = (0 < x + (y::real))"
-  by arith
-
-lemma "(x < -y) = (x + y < (0::real))"
-  by arith
-
-lemma "(y < x + -z) = (y + z < (x::real))"
-  by arith
-
-lemma "(x + -y < z) = (x < z + (y::real))"
-  by arith
-
-lemma "x \<le> y ==> x < y + (1::real)"
-  by arith
-
-lemma "(x - y) + y = (x::real)"
-  by arith
-
-lemma "y + (x - y) = (x::real)"
-  by arith
-
-lemma "x - x = (0::real)"
-  by arith
-
-lemma "(x - y = 0) = (x = (y::real))"
-  by arith
-
-lemma "((0::real) \<le> x + x) = (0 \<le> x)"
-  by arith
-
-lemma "(-x \<le> x) = ((0::real) \<le> x)"
-  by arith
-
-lemma "(x \<le> -x) = (x \<le> (0::real))"
-  by arith
-
-lemma "(-x = (0::real)) = (x = 0)"
-  by arith
-
-lemma "-(x - y) = y - (x::real)"
-  by arith
-
-lemma "((0::real) < x - y) = (y < x)"
-  by arith
-
-lemma "((0::real) \<le> x - y) = (y \<le> x)"
-  by arith
-
-lemma "(x + y) - x = (y::real)"
-  by arith
-
-lemma "(-x = y) = (x = (-y::real))"
-  by arith
-
-lemma "x < (y::real) ==> \<not>(x = y)"
-  by arith
-
-lemma "(x \<le> x + y) = ((0::real) \<le> y)"
-  by arith
-
-lemma "(y \<le> x + y) = ((0::real) \<le> x)"
-  by arith
-
-lemma "(x < x + y) = ((0::real) < y)"
-  by arith
-
-lemma "(y < x + y) = ((0::real) < x)"
-  by arith
-
-lemma "(x - y) - x = (-y::real)"
-  by arith
-
-lemma "(x + y < z) = (x < z - (y::real))"
-  by arith
-
-lemma "(x - y < z) = (x < z + (y::real))"
-  by arith
-
-lemma "(x < y - z) = (x + z < (y::real))"
-  by arith
-
-lemma "(x \<le> y - z) = (x + z \<le> (y::real))"
-  by arith
-
-lemma "(x - y \<le> z) = (x \<le> z + (y::real))"
-  by arith
-
-lemma "(-x < -y) = (y < (x::real))"
-  by arith
-
-lemma "(-x \<le> -y) = (y \<le> (x::real))"
-  by arith
-
-lemma "(a + b) - (c + d) = (a - c) + (b - (d::real))"
-  by arith
-
-lemma "(0::real) - x = -x"
-  by arith
-
-lemma "x - (0::real) = x"
-  by arith
-
-lemma "w \<le> x \<and> y < z ==> w + y < x + (z::real)"
-  by arith
-
-lemma "w < x \<and> y \<le> z ==> w + y < x + (z::real)"
-  by arith
-
-lemma "(0::real) \<le> x \<and> 0 < y ==> 0 < x + (y::real)"
-  by arith
-
-lemma "(0::real) < x \<and> 0 \<le> y ==> 0 < x + y"
-  by arith
-
-lemma "-x - y = -(x + (y::real))"
-  by arith
-
-lemma "x - (-y) = x + (y::real)"
-  by arith
-
-lemma "-x - -y = y - (x::real)"
-  by arith
-
-lemma "(a - b) + (b - c) = a - (c::real)"
-  by arith
-
-lemma "(x = y - z) = (x + z = (y::real))"
-  by arith
-
-lemma "(x - y = z) = (x = z + (y::real))"
-  by arith
-
-lemma "x - (x - y) = (y::real)"
-  by arith
-
-lemma "x - (x + y) = -(y::real)"
-  by arith
-
-lemma "x = y ==> x \<le> (y::real)"
-  by arith
-
-lemma "(0::real) < x ==> \<not>(x = 0)"
-  by arith
-
-lemma "(x + y) * (x - y) = (x * x) - (y * y)"
-  oops
-
-lemma "(-x = -y) = (x = (y::real))"
-  by arith
-
-lemma "(-x < -y) = (y < (x::real))"
-  by arith
-
-lemma "!!a::real. a \<le> b ==> c \<le> d ==> x + y < z ==> a + c \<le> b + d"
-  by (tactic "fast_arith_tac 1")
-
-lemma "!!a::real. a < b ==> c < d ==> a - d \<le> b + (-c)"
-  by (tactic "fast_arith_tac 1")
-
-lemma "!!a::real. a \<le> b ==> b + b \<le> c ==> a + a \<le> c"
-  by (tactic "fast_arith_tac 1")
-
-lemma "!!a::real. a + b \<le> i + j ==> a \<le> b ==> i \<le> j ==> a + a \<le> j + j"
-  by (tactic "fast_arith_tac 1")
-
-lemma "!!a::real. a + b < i + j ==> a < b ==> i < j ==> a + a < j + j"
-  by (tactic "fast_arith_tac 1")
-
-lemma "!!a::real. a + b + c \<le> i + j + k \<and> a \<le> b \<and> b \<le> c \<and> i \<le> j \<and> j \<le> k --> a + a + a \<le> k + k + k"
-  by arith
-
-lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c
-    ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a \<le> l"
-  by (tactic "fast_arith_tac 1")
-
-lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c
-    ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a + a + a + a \<le> l + l + l + l"
-  by (tactic "fast_arith_tac 1")
-
-lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c
-    ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a + a + a + a + a \<le> l + l + l + l + i"
-  by (tactic "fast_arith_tac 1")
-
-lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c
-    ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a + a + a + a + a + a \<le> l + l + l + l + i + l"
-  by (tactic "fast_arith_tac 1")
-
-end
diff -r 46ad7fd03a38 -r 2160abf7cfe7 src/HOL/Real/ex/ROOT.ML
--- a/src/HOL/Real/ex/ROOT.ML	Tue May 06 12:29:49 2003 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,7 +0,0 @@
-(*  Title:      HOL/Real/ex/ROOT.ML
-    ID:         $Id$
-
-Miscellaneous HOL-Real Examples.
-*)
-
-time_use_thy "BinEx";