# HG changeset patch
# User wenzelm
# Date 937927740 -7200
# Node ID 8519d50193090b573ceffba21d2982693a7cb8bd
# Parent  ff8dbd0589aa6215c19b003bf14db31115af202e
tuned;

diff -r ff8dbd0589aa -r 8519d5019309 src/HOL/Real/Lubs.thy
--- a/src/HOL/Real/Lubs.thy	Tue Sep 21 17:28:33 1999 +0200
+++ b/src/HOL/Real/Lubs.thy	Tue Sep 21 17:29:00 1999 +0200
@@ -7,7 +7,7 @@
 *) 
 
 
-Lubs = Set +
+Lubs = Main +
 
 consts
     
diff -r ff8dbd0589aa -r 8519d5019309 src/HOL/Real/PNat.ML
--- a/src/HOL/Real/PNat.ML	Tue Sep 21 17:28:33 1999 +0200
+++ b/src/HOL/Real/PNat.ML	Tue Sep 21 17:29:00 1999 +0200
@@ -86,8 +86,6 @@
 by (rtac Rep_pnat_inverse 1);
 qed "inj_Rep_pnat";
 
-bind_thm ("Zero_not_Suc", Suc_not_Zero RS not_sym);
-
 Goal "0 ~: pnat";
 by (stac pnat_unfold 1);
 by Auto_tac;
diff -r ff8dbd0589aa -r 8519d5019309 src/HOL/Real/PNat.thy
--- a/src/HOL/Real/PNat.thy	Tue Sep 21 17:28:33 1999 +0200
+++ b/src/HOL/Real/PNat.thy	Tue Sep 21 17:29:00 1999 +0200
@@ -44,28 +44,3 @@
        "x <= (y::pnat) ==  ~(y < x)"
 
 end
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
diff -r ff8dbd0589aa -r 8519d5019309 src/HOL/Real/Real.thy
--- a/src/HOL/Real/Real.thy	Tue Sep 21 17:28:33 1999 +0200
+++ b/src/HOL/Real/Real.thy	Tue Sep 21 17:29:00 1999 +0200
@@ -1,2 +1,2 @@
 
-Real = RComplete
+Real = Main + RComplete
diff -r ff8dbd0589aa -r 8519d5019309 src/HOL/Real/RealOrd.ML
--- a/src/HOL/Real/RealOrd.ML	Tue Sep 21 17:28:33 1999 +0200
+++ b/src/HOL/Real/RealOrd.ML	Tue Sep 21 17:29:00 1999 +0200
@@ -775,31 +775,38 @@
 qed "real_of_nat_eq_cancel";
 
 (*------- lemmas -------*)
-goal NatDef.thy "!!m. [| m < Suc n; n <= m |] ==> m = n";
+context NatDef.thy;
+
+Goal "!!m. [| m < Suc n; n <= m |] ==> m = n";
 by (auto_tac (claset() addSDs [le_imp_less_or_eq] addIs [less_asym],
 	      simpset() addsimps [less_Suc_eq]));
 qed "lemma_nat_not_dense";
 
-goal NatDef.thy "!!m. [| m <= Suc n; n < m |] ==> m = Suc n";
+Goal "!!m. [| m <= Suc n; n < m |] ==> m = Suc n";
 by (auto_tac (claset() addSDs [le_imp_less_or_eq] addIs [less_asym],
 	      simpset() addsimps [le_Suc_eq]));
 qed "lemma_nat_not_dense2";
 
-goal NatDef.thy "!!m. m < Suc n ==> ~ Suc n <= m";
+Goal "!!m. m < Suc n ==> ~ Suc n <= m";
 by (blast_tac (claset() addDs [less_le_trans] addIs [less_asym]) 1);
 qed "lemma_not_leI";
 
-goalw NatDef.thy [le_def] "!!m. ~ Suc n <= m ==> ~ Suc (Suc n) <= m";
+Goalw [le_def] "!!m. ~ Suc n <= m ==> ~ Suc (Suc n) <= m";
 by Auto_tac;
 qed "lemma_not_leI2";
 
 (*------- lemmas -------*)
-val [prem] = goal Arith.thy "n < Suc(m) ==> Suc(m)-n = Suc(m-n)";
-by (rtac (prem RS rev_mp) 1);
+context Arith.thy;
+
+Goal "n < Suc(m) ==> Suc(m)-n = Suc(m-n)";
+by (dtac rev_mp 1);
 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
 by (ALLGOALS Asm_simp_tac);
 qed "Suc_diff_n";
 
+
+context thy;
+
 (* Goalw  [real_of_nat_def] 
    "real_of_nat (n1 - n2) = real_of_nat n1 + -real_of_nat n2";*)
 
@@ -813,5 +820,3 @@
 by (asm_full_simp_tac (simpset() addsimps [real_of_nat_one RS sym,
 					   real_of_nat_add,Suc_diff_n]) 1);
 qed "real_of_nat_minus";
-
-
diff -r ff8dbd0589aa -r 8519d5019309 src/HOL/TLA/TLA.thy
--- a/src/HOL/TLA/TLA.thy	Tue Sep 21 17:28:33 1999 +0200
+++ b/src/HOL/TLA/TLA.thy	Tue Sep 21 17:29:00 1999 +0200
@@ -9,7 +9,7 @@
 The temporal level of TLA.
 *)
 
-TLA  =  Init + WF_Rel +
+TLA  =  Init +
 
 consts
   (** abstract syntax **)
@@ -92,5 +92,3 @@
 	      |] ==> G sigma"
   history    "|- EEX h. Init(h = ha) & [](!x. $h = #x --> h` = hb x)"
 end
-
-ML