# HG changeset patch
# User paulson
# Date 934821692 -7200
# Node ID 4e3f386c2e379975f687e39e186095ae9be56f18
# Parent  bfa767b4dc516bedb1d0133f28ecee12883e6730
inserted Id: lines

diff -r bfa767b4dc51 -r 4e3f386c2e37 src/HOL/Real/Hyperreal/Filter.ML
--- a/src/HOL/Real/Hyperreal/Filter.ML	Mon Aug 16 18:41:06 1999 +0200
+++ b/src/HOL/Real/Hyperreal/Filter.ML	Mon Aug 16 18:41:32 1999 +0200
@@ -1,4 +1,5 @@
 (*  Title       : Filter.ML
+    ID          : $Id$
     Author      : Jacques D. Fleuriot
     Copyright   : 1998  University of Cambridge
     Description : Filters and Ultrafilter
diff -r bfa767b4dc51 -r 4e3f386c2e37 src/HOL/Real/Hyperreal/Filter.thy
--- a/src/HOL/Real/Hyperreal/Filter.thy	Mon Aug 16 18:41:06 1999 +0200
+++ b/src/HOL/Real/Hyperreal/Filter.thy	Mon Aug 16 18:41:32 1999 +0200
@@ -1,4 +1,5 @@
 (*  Title       : Filter.thy
+    ID          : $Id$
     Author      : Jacques D. Fleuriot
     Copyright   : 1998  University of Cambridge
     Description : Filters and Ultrafilters
diff -r bfa767b4dc51 -r 4e3f386c2e37 src/HOL/Real/Hyperreal/Zorn.ML
--- a/src/HOL/Real/Hyperreal/Zorn.ML	Mon Aug 16 18:41:06 1999 +0200
+++ b/src/HOL/Real/Hyperreal/Zorn.ML	Mon Aug 16 18:41:32 1999 +0200
@@ -1,11 +1,10 @@
 (*  Title       : Zorn.ML
+    ID          : $Id$
     Author      : Jacques D. Fleuriot
     Copyright   : 1998  University of Cambridge
     Description : Zorn's Lemma -- adapted proofs from lcp's ZF/Zorn.ML
 *) 
 
-open Zorn;
-
 (*---------------------------------------------------------------
       Section 1.  Mathematical Preamble 
  ---------------------------------------------------------------*)
diff -r bfa767b4dc51 -r 4e3f386c2e37 src/HOL/Real/Hyperreal/Zorn.thy
--- a/src/HOL/Real/Hyperreal/Zorn.thy	Mon Aug 16 18:41:06 1999 +0200
+++ b/src/HOL/Real/Hyperreal/Zorn.thy	Mon Aug 16 18:41:32 1999 +0200
@@ -1,4 +1,5 @@
 (*  Title       : Zorn.thy
+    ID          : $Id$
     Author      : Jacques D. Fleuriot
     Copyright   : 1998  University of Cambridge
     Description : Zorn's Lemma -- See lcp's Zorn.thy in ZF
diff -r bfa767b4dc51 -r 4e3f386c2e37 src/HOL/Real/Lubs.ML
--- a/src/HOL/Real/Lubs.ML	Mon Aug 16 18:41:06 1999 +0200
+++ b/src/HOL/Real/Lubs.ML	Mon Aug 16 18:41:32 1999 +0200
@@ -1,12 +1,11 @@
 (*  Title       : Lubs.ML
+    ID          : $Id$
     Author      : Jacques D. Fleuriot
     Copyright   : 1998  University of Cambridge
     Description : Completeness of the reals. A few of the 
                   definitions suggested by James Margetson
 *) 
 
-open Lubs;
-
 (*------------------------------------------------------------------------
                         Rules for *<= and <=*
  ------------------------------------------------------------------------*)
diff -r bfa767b4dc51 -r 4e3f386c2e37 src/HOL/Real/Lubs.thy
--- a/src/HOL/Real/Lubs.thy	Mon Aug 16 18:41:06 1999 +0200
+++ b/src/HOL/Real/Lubs.thy	Mon Aug 16 18:41:32 1999 +0200
@@ -1,4 +1,5 @@
 (*  Title       : Lubs.thy
+    ID          : $Id$
     Author      : Jacques D. Fleuriot
     Copyright   : 1998  University of Cambridge
     Description : Upper bounds, lubs definitions
diff -r bfa767b4dc51 -r 4e3f386c2e37 src/HOL/Real/PNat.ML
--- a/src/HOL/Real/PNat.ML	Mon Aug 16 18:41:06 1999 +0200
+++ b/src/HOL/Real/PNat.ML	Mon Aug 16 18:41:32 1999 +0200
@@ -1,12 +1,11 @@
 (*  Title       : PNat.ML
+    ID          : $Id$
     Author      : Jacques D. Fleuriot
     Copyright   : 1998  University of Cambridge
     Description : The positive naturals -- proofs 
                 : mainly as in Nat.thy
 *)
 
-open PNat;
-
 Goal "mono(%X. {1} Un (Suc``X))";
 by (REPEAT (ares_tac [monoI, subset_refl, image_mono, Un_mono] 1));
 qed "pnat_fun_mono";
diff -r bfa767b4dc51 -r 4e3f386c2e37 src/HOL/Real/PNat.thy
--- a/src/HOL/Real/PNat.thy	Mon Aug 16 18:41:06 1999 +0200
+++ b/src/HOL/Real/PNat.thy	Mon Aug 16 18:41:32 1999 +0200
@@ -1,4 +1,5 @@
 (*  Title       : PNat.thy
+    ID          : $Id$
     Author      : Jacques D. Fleuriot
     Copyright   : 1998  University of Cambridge
     Description : The positive naturals
diff -r bfa767b4dc51 -r 4e3f386c2e37 src/HOL/Real/PRat.ML
--- a/src/HOL/Real/PRat.ML	Mon Aug 16 18:41:06 1999 +0200
+++ b/src/HOL/Real/PRat.ML	Mon Aug 16 18:41:32 1999 +0200
@@ -1,18 +1,16 @@
 (*  Title       : PRat.ML
+    ID          : $Id$
     Author      : Jacques D. Fleuriot
     Copyright   : 1998  University of Cambridge
     Description : The positive rationals
 *) 
 
-open PRat;
-
 Delrules [equalityI];
 
 (*** Many theorems similar to those in Integ.thy ***)
 (*** Proving that ratrel is an equivalence relation ***)
 
-Goal
-    "[| (x1::pnat) * y2 = x2 * y1; x2 * y3 = x3 * y2 |] \
+Goal "[| (x1::pnat) * y2 = x2 * y1; x2 * y3 = x3 * y2 |] \
 \            ==> x1 * y3 = x3 * y1";        
 by (res_inst_tac [("k1","y2")] (pnat_mult_cancel1 RS iffD1) 1);
 by (auto_tac (claset(), simpset() addsimps [pnat_mult_assoc RS sym]));
@@ -155,8 +153,7 @@
 by (auto_tac (claset(),simpset() addsimps [pnat_mult_assoc RS sym]));
 qed "prat_add_congruent2_lemma";
 
-Goal 
-    "congruent2 ratrel (%p1 p2.                  \
+Goal "congruent2 ratrel (%p1 p2.                  \
 \         split (%x1 y1. split (%x2 y2. ratrel^^{(x1*y2 + x2*y1, y1*y2)}) p2) p1)";
 by (rtac (equiv_ratrel RS congruent2_commuteI) 1);
 by Safe_tac;
@@ -451,8 +448,7 @@
 by (auto_tac (claset(),simpset() addsimps prat_add_ac));
 qed "prat_add_less2_mono1";
 
-Goal  
-      "!!(q1::prat). q1 < q2 ==> x + q1 < x + q2";
+Goal "!!(q1::prat). q1 < q2 ==> x + q1 < x + q2";
 by (auto_tac (claset() addIs [prat_add_less2_mono1],
     simpset() addsimps [prat_add_commute]));
 qed "prat_add_less2_mono2";
@@ -509,16 +505,14 @@
 by (asm_full_simp_tac (simpset() addsimps pnat_mult_ac) 1);
 qed "prat_linear";
 
-Goal
-    "!!(q1::prat). [| q1 < q2 ==> P;  q1 = q2 ==> P; \
+Goal "!!(q1::prat). [| q1 < q2 ==> P;  q1 = q2 ==> P; \
 \          q2 < q1 ==> P |] ==> P";
 by (cut_inst_tac [("q1.0","q1"),("q2.0","q2")] prat_linear 1);
 by Auto_tac;
 qed "prat_linear_less2";
 
 (* Gleason p. 120 -- 9-2.6 (iv) *)
-Goal 
- "!!(q1::prat). [| q1 < q2; qinv(q1) = qinv(q2) |] ==> P";
+Goal "!!(q1::prat). [| q1 < q2; qinv(q1) = qinv(q2) |] ==> P";
 by (cut_inst_tac [("x","qinv (q2)"),("q1.0","q1"),
    ("q2.0","q2")] prat_mult_less2_mono1 1);
 by (assume_tac 1);
@@ -526,8 +520,7 @@
 by (auto_tac (claset(),simpset() addsimps [prat_less_not_refl]));
 qed "lemma1_qinv_prat_less";
 
-Goal 
- "!!(q1::prat). [| q1 < q2; qinv(q1) < qinv(q2) |] ==> P";
+Goal "!!(q1::prat). [| q1 < q2; qinv(q1) < qinv(q2) |] ==> P";
 by (cut_inst_tac [("x","qinv (q2)"),("q1.0","q1"),
    ("q2.0","q2")] prat_mult_less2_mono1 1);
 by (assume_tac 1);
@@ -539,8 +532,7 @@
     [prat_less_not_refl]));
 qed "lemma2_qinv_prat_less";
 
-Goal 
-      "!!(q1::prat). q1 < q2  ==> qinv (q2) < qinv (q1)";
+Goal "!!(q1::prat). q1 < q2  ==> qinv (q2) < qinv (q1)";
 by (res_inst_tac [("q2.0","qinv q1"),
          ("q1.0","qinv q2")] prat_linear_less2 1);
 by (auto_tac (claset() addEs [lemma1_qinv_prat_less,
@@ -693,8 +685,7 @@
     simpset() addsimps [prat_mult_commute]));
 qed "prat_mult_le2_mono1";
 
-Goal 
-      "!!(q1::prat). q1 <= q2  ==> qinv (q2) <= qinv (q1)";
+Goal "!!(q1::prat). q1 <= q2  ==> qinv (q2) <= qinv (q1)";
 by (dtac prat_le_imp_less_or_eq 1);
 by (Step_tac 1);
 by (auto_tac (claset() addSIs [prat_le_refl,
diff -r bfa767b4dc51 -r 4e3f386c2e37 src/HOL/Real/PRat.thy
--- a/src/HOL/Real/PRat.thy	Mon Aug 16 18:41:06 1999 +0200
+++ b/src/HOL/Real/PRat.thy	Mon Aug 16 18:41:32 1999 +0200
@@ -1,4 +1,5 @@
 (*  Title       : PRat.thy
+    ID          : $Id$
     Author      : Jacques D. Fleuriot
     Copyright   : 1998  University of Cambridge
     Description : The positive rationals
diff -r bfa767b4dc51 -r 4e3f386c2e37 src/HOL/Real/PReal.ML
--- a/src/HOL/Real/PReal.ML	Mon Aug 16 18:41:06 1999 +0200
+++ b/src/HOL/Real/PReal.ML	Mon Aug 16 18:41:32 1999 +0200
@@ -1,4 +1,5 @@
 (*  Title       : PReal.ML
+    ID          : $Id$
     Author      : Jacques D. Fleuriot
     Copyright   : 1998  University of Cambridge
     Description : The positive reals as Dedekind sections of positive
@@ -8,8 +9,6 @@
 
 claset_ref() := claset() delWrapper "bspec";
 
-open PReal;
-
 Goal "inj_on Abs_preal preal";
 by (rtac inj_on_inverseI 1);
 by (etac Abs_preal_inverse 1);
diff -r bfa767b4dc51 -r 4e3f386c2e37 src/HOL/Real/PReal.thy
--- a/src/HOL/Real/PReal.thy	Mon Aug 16 18:41:06 1999 +0200
+++ b/src/HOL/Real/PReal.thy	Mon Aug 16 18:41:32 1999 +0200
@@ -1,4 +1,5 @@
-(*   Title       : PReal.thy
+(*  Title       : PReal.thy
+    ID          : $Id$
     Author      : Jacques D. Fleuriot
     Copyright   : 1998  University of Cambridge
     Description : The positive reals as Dedekind sections of positive
diff -r bfa767b4dc51 -r 4e3f386c2e37 src/HOL/Real/RComplete.ML
--- a/src/HOL/Real/RComplete.ML	Mon Aug 16 18:41:06 1999 +0200
+++ b/src/HOL/Real/RComplete.ML	Mon Aug 16 18:41:32 1999 +0200
@@ -1,4 +1,5 @@
 (*  Title       : RComplete.thy
+    ID          : $Id$
     Author      : Jacques D. Fleuriot
     Copyright   : 1998  University of Cambridge
     Description : Completeness theorems for positive
diff -r bfa767b4dc51 -r 4e3f386c2e37 src/HOL/Real/RComplete.thy
--- a/src/HOL/Real/RComplete.thy	Mon Aug 16 18:41:06 1999 +0200
+++ b/src/HOL/Real/RComplete.thy	Mon Aug 16 18:41:32 1999 +0200
@@ -1,4 +1,5 @@
 (*  Title       : RComplete.thy
+    ID          : $Id$
     Author      : Jacques D. Fleuriot
     Copyright   : 1998  University of Cambridge
     Description : Completeness theorems for positive
diff -r bfa767b4dc51 -r 4e3f386c2e37 src/HOL/Real/ROOT.ML
--- a/src/HOL/Real/ROOT.ML	Mon Aug 16 18:41:06 1999 +0200
+++ b/src/HOL/Real/ROOT.ML	Mon Aug 16 18:41:32 1999 +0200
@@ -14,3 +14,4 @@
 time_use_thy "RealAbs";
 time_use_thy "RComplete";
 time_use_thy "Hyperreal/Filter";
+time_use_thy "Hyperreal/HyperDef";
diff -r bfa767b4dc51 -r 4e3f386c2e37 src/HOL/Real/Real.ML
--- a/src/HOL/Real/Real.ML	Mon Aug 16 18:41:06 1999 +0200
+++ b/src/HOL/Real/Real.ML	Mon Aug 16 18:41:32 1999 +0200
@@ -1,4 +1,5 @@
 (*  Title:       HOL/Real/Real.ML
+    ID:          $Id$
     Author:      Lawrence C. Paulson
                  Jacques D. Fleuriot
     Copyright:   1998  University of Cambridge
diff -r bfa767b4dc51 -r 4e3f386c2e37 src/HOL/Real/Real.thy
--- a/src/HOL/Real/Real.thy	Mon Aug 16 18:41:06 1999 +0200
+++ b/src/HOL/Real/Real.thy	Mon Aug 16 18:41:32 1999 +0200
@@ -1,4 +1,5 @@
 (*  Title:       Real/Real.thy
+    ID          : $Id$
     Author:      Lawrence C. Paulson
                  Jacques D. Fleuriot
     Copyright:   1998  University of Cambridge
diff -r bfa767b4dc51 -r 4e3f386c2e37 src/HOL/Real/RealAbs.ML
--- a/src/HOL/Real/RealAbs.ML	Mon Aug 16 18:41:06 1999 +0200
+++ b/src/HOL/Real/RealAbs.ML	Mon Aug 16 18:41:32 1999 +0200
@@ -1,4 +1,5 @@
 (*  Title       : RealAbs.ML
+    ID          : $Id$
     Author      : Jacques D. Fleuriot
     Copyright   : 1998  University of Cambridge
     Description : Absolute value function for the reals
diff -r bfa767b4dc51 -r 4e3f386c2e37 src/HOL/Real/RealAbs.thy
--- a/src/HOL/Real/RealAbs.thy	Mon Aug 16 18:41:06 1999 +0200
+++ b/src/HOL/Real/RealAbs.thy	Mon Aug 16 18:41:32 1999 +0200
@@ -1,4 +1,5 @@
 (*  Title       : RealAbs.thy
+    ID          : $Id$
     Author      : Jacques D. Fleuriot
     Copyright   : 1998  University of Cambridge
     Description : Absolute value function for the reals
diff -r bfa767b4dc51 -r 4e3f386c2e37 src/HOL/Real/RealDef.ML
--- a/src/HOL/Real/RealDef.ML	Mon Aug 16 18:41:06 1999 +0200
+++ b/src/HOL/Real/RealDef.ML	Mon Aug 16 18:41:32 1999 +0200
@@ -1,4 +1,5 @@
 (*  Title       : Real/RealDef.ML
+    ID          : $Id$
     Author      : Jacques D. Fleuriot
     Copyright   : 1998  University of Cambridge
     Description : The reals
diff -r bfa767b4dc51 -r 4e3f386c2e37 src/HOL/Real/RealDef.thy
--- a/src/HOL/Real/RealDef.thy	Mon Aug 16 18:41:06 1999 +0200
+++ b/src/HOL/Real/RealDef.thy	Mon Aug 16 18:41:32 1999 +0200
@@ -1,4 +1,5 @@
 (*  Title       : Real/RealDef.thy
+    ID          : $Id$
     Author      : Jacques D. Fleuriot
     Copyright   : 1998  University of Cambridge
     Description : The reals
diff -r bfa767b4dc51 -r 4e3f386c2e37 src/HOL/Real/RealPow.ML
--- a/src/HOL/Real/RealPow.ML	Mon Aug 16 18:41:06 1999 +0200
+++ b/src/HOL/Real/RealPow.ML	Mon Aug 16 18:41:32 1999 +0200
@@ -1,4 +1,5 @@
 (*  Title       : RealPow.ML
+    ID          : $Id$
     Author      : Jacques D. Fleuriot  
     Copyright   : 1998  University of Cambridge
     Description : Natural Powers of reals theory
diff -r bfa767b4dc51 -r 4e3f386c2e37 src/HOL/Real/RealPow.thy
--- a/src/HOL/Real/RealPow.thy	Mon Aug 16 18:41:06 1999 +0200
+++ b/src/HOL/Real/RealPow.thy	Mon Aug 16 18:41:32 1999 +0200
@@ -1,4 +1,5 @@
 (*  Title       : RealPow.thy
+    ID          : $Id$
     Author      : Jacques D. Fleuriot  
     Copyright   : 1998  University of Cambridge
     Description : Natural powers theory