tuned;
authorwenzelm
Tue Sep 21 17:29:00 1999 +0200 (1999-09-21 ago)
changeset 75628519d5019309
parent 7561 ff8dbd0589aa
child 7563 26ca52846865
tuned;
src/HOL/Real/Lubs.thy
src/HOL/Real/PNat.ML
src/HOL/Real/PNat.thy
src/HOL/Real/Real.thy
src/HOL/Real/RealOrd.ML
src/HOL/TLA/TLA.thy
     1.1 --- a/src/HOL/Real/Lubs.thy	Tue Sep 21 17:28:33 1999 +0200
     1.2 +++ b/src/HOL/Real/Lubs.thy	Tue Sep 21 17:29:00 1999 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  *) 
     1.5  
     1.6  
     1.7 -Lubs = Set +
     1.8 +Lubs = Main +
     1.9  
    1.10  consts
    1.11      
     2.1 --- a/src/HOL/Real/PNat.ML	Tue Sep 21 17:28:33 1999 +0200
     2.2 +++ b/src/HOL/Real/PNat.ML	Tue Sep 21 17:29:00 1999 +0200
     2.3 @@ -86,8 +86,6 @@
     2.4  by (rtac Rep_pnat_inverse 1);
     2.5  qed "inj_Rep_pnat";
     2.6  
     2.7 -bind_thm ("Zero_not_Suc", Suc_not_Zero RS not_sym);
     2.8 -
     2.9  Goal "0 ~: pnat";
    2.10  by (stac pnat_unfold 1);
    2.11  by Auto_tac;
     3.1 --- a/src/HOL/Real/PNat.thy	Tue Sep 21 17:28:33 1999 +0200
     3.2 +++ b/src/HOL/Real/PNat.thy	Tue Sep 21 17:29:00 1999 +0200
     3.3 @@ -44,28 +44,3 @@
     3.4         "x <= (y::pnat) ==  ~(y < x)"
     3.5  
     3.6  end
     3.7 -
     3.8 -
     3.9 -
    3.10 -
    3.11 -
    3.12 -
    3.13 -
    3.14 -
    3.15 -
    3.16 -
    3.17 -
    3.18 -
    3.19 -
    3.20 -
    3.21 -
    3.22 -
    3.23 -
    3.24 -
    3.25 -
    3.26 -
    3.27 -
    3.28 -
    3.29 -
    3.30 -
    3.31 -
     4.1 --- a/src/HOL/Real/Real.thy	Tue Sep 21 17:28:33 1999 +0200
     4.2 +++ b/src/HOL/Real/Real.thy	Tue Sep 21 17:29:00 1999 +0200
     4.3 @@ -1,2 +1,2 @@
     4.4  
     4.5 -Real = RComplete
     4.6 +Real = Main + RComplete
     5.1 --- a/src/HOL/Real/RealOrd.ML	Tue Sep 21 17:28:33 1999 +0200
     5.2 +++ b/src/HOL/Real/RealOrd.ML	Tue Sep 21 17:29:00 1999 +0200
     5.3 @@ -775,31 +775,38 @@
     5.4  qed "real_of_nat_eq_cancel";
     5.5  
     5.6  (*------- lemmas -------*)
     5.7 -goal NatDef.thy "!!m. [| m < Suc n; n <= m |] ==> m = n";
     5.8 +context NatDef.thy;
     5.9 +
    5.10 +Goal "!!m. [| m < Suc n; n <= m |] ==> m = n";
    5.11  by (auto_tac (claset() addSDs [le_imp_less_or_eq] addIs [less_asym],
    5.12  	      simpset() addsimps [less_Suc_eq]));
    5.13  qed "lemma_nat_not_dense";
    5.14  
    5.15 -goal NatDef.thy "!!m. [| m <= Suc n; n < m |] ==> m = Suc n";
    5.16 +Goal "!!m. [| m <= Suc n; n < m |] ==> m = Suc n";
    5.17  by (auto_tac (claset() addSDs [le_imp_less_or_eq] addIs [less_asym],
    5.18  	      simpset() addsimps [le_Suc_eq]));
    5.19  qed "lemma_nat_not_dense2";
    5.20  
    5.21 -goal NatDef.thy "!!m. m < Suc n ==> ~ Suc n <= m";
    5.22 +Goal "!!m. m < Suc n ==> ~ Suc n <= m";
    5.23  by (blast_tac (claset() addDs [less_le_trans] addIs [less_asym]) 1);
    5.24  qed "lemma_not_leI";
    5.25  
    5.26 -goalw NatDef.thy [le_def] "!!m. ~ Suc n <= m ==> ~ Suc (Suc n) <= m";
    5.27 +Goalw [le_def] "!!m. ~ Suc n <= m ==> ~ Suc (Suc n) <= m";
    5.28  by Auto_tac;
    5.29  qed "lemma_not_leI2";
    5.30  
    5.31  (*------- lemmas -------*)
    5.32 -val [prem] = goal Arith.thy "n < Suc(m) ==> Suc(m)-n = Suc(m-n)";
    5.33 -by (rtac (prem RS rev_mp) 1);
    5.34 +context Arith.thy;
    5.35 +
    5.36 +Goal "n < Suc(m) ==> Suc(m)-n = Suc(m-n)";
    5.37 +by (dtac rev_mp 1);
    5.38  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    5.39  by (ALLGOALS Asm_simp_tac);
    5.40  qed "Suc_diff_n";
    5.41  
    5.42 +
    5.43 +context thy;
    5.44 +
    5.45  (* Goalw  [real_of_nat_def] 
    5.46     "real_of_nat (n1 - n2) = real_of_nat n1 + -real_of_nat n2";*)
    5.47  
    5.48 @@ -813,5 +820,3 @@
    5.49  by (asm_full_simp_tac (simpset() addsimps [real_of_nat_one RS sym,
    5.50  					   real_of_nat_add,Suc_diff_n]) 1);
    5.51  qed "real_of_nat_minus";
    5.52 -
    5.53 -
     6.1 --- a/src/HOL/TLA/TLA.thy	Tue Sep 21 17:28:33 1999 +0200
     6.2 +++ b/src/HOL/TLA/TLA.thy	Tue Sep 21 17:29:00 1999 +0200
     6.3 @@ -9,7 +9,7 @@
     6.4  The temporal level of TLA.
     6.5  *)
     6.6  
     6.7 -TLA  =  Init + WF_Rel +
     6.8 +TLA  =  Init +
     6.9  
    6.10  consts
    6.11    (** abstract syntax **)
    6.12 @@ -92,5 +92,3 @@
    6.13  	      |] ==> G sigma"
    6.14    history    "|- EEX h. Init(h = ha) & [](!x. $h = #x --> h` = hb x)"
    6.15  end
    6.16 -
    6.17 -ML