--- 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
--- 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
--- 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
---------------------------------------------------------------*)
--- 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
--- 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 <=*
------------------------------------------------------------------------*)
--- 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
--- 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";
--- 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
--- 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,
--- 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
--- 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);
--- 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
--- 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
--- 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
--- 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";
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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