src/HOL/Real/RealOrd.ML
changeset 7562 8519d5019309
parent 7499 23e090051cb8
child 8742 8a5b3f58b944
     1.1 --- a/src/HOL/Real/RealOrd.ML	Tue Sep 21 17:28:33 1999 +0200
     1.2 +++ b/src/HOL/Real/RealOrd.ML	Tue Sep 21 17:29:00 1999 +0200
     1.3 @@ -775,31 +775,38 @@
     1.4  qed "real_of_nat_eq_cancel";
     1.5  
     1.6  (*------- lemmas -------*)
     1.7 -goal NatDef.thy "!!m. [| m < Suc n; n <= m |] ==> m = n";
     1.8 +context NatDef.thy;
     1.9 +
    1.10 +Goal "!!m. [| m < Suc n; n <= m |] ==> m = n";
    1.11  by (auto_tac (claset() addSDs [le_imp_less_or_eq] addIs [less_asym],
    1.12  	      simpset() addsimps [less_Suc_eq]));
    1.13  qed "lemma_nat_not_dense";
    1.14  
    1.15 -goal NatDef.thy "!!m. [| m <= Suc n; n < m |] ==> m = Suc n";
    1.16 +Goal "!!m. [| m <= Suc n; n < m |] ==> m = Suc n";
    1.17  by (auto_tac (claset() addSDs [le_imp_less_or_eq] addIs [less_asym],
    1.18  	      simpset() addsimps [le_Suc_eq]));
    1.19  qed "lemma_nat_not_dense2";
    1.20  
    1.21 -goal NatDef.thy "!!m. m < Suc n ==> ~ Suc n <= m";
    1.22 +Goal "!!m. m < Suc n ==> ~ Suc n <= m";
    1.23  by (blast_tac (claset() addDs [less_le_trans] addIs [less_asym]) 1);
    1.24  qed "lemma_not_leI";
    1.25  
    1.26 -goalw NatDef.thy [le_def] "!!m. ~ Suc n <= m ==> ~ Suc (Suc n) <= m";
    1.27 +Goalw [le_def] "!!m. ~ Suc n <= m ==> ~ Suc (Suc n) <= m";
    1.28  by Auto_tac;
    1.29  qed "lemma_not_leI2";
    1.30  
    1.31  (*------- lemmas -------*)
    1.32 -val [prem] = goal Arith.thy "n < Suc(m) ==> Suc(m)-n = Suc(m-n)";
    1.33 -by (rtac (prem RS rev_mp) 1);
    1.34 +context Arith.thy;
    1.35 +
    1.36 +Goal "n < Suc(m) ==> Suc(m)-n = Suc(m-n)";
    1.37 +by (dtac rev_mp 1);
    1.38  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    1.39  by (ALLGOALS Asm_simp_tac);
    1.40  qed "Suc_diff_n";
    1.41  
    1.42 +
    1.43 +context thy;
    1.44 +
    1.45  (* Goalw  [real_of_nat_def] 
    1.46     "real_of_nat (n1 - n2) = real_of_nat n1 + -real_of_nat n2";*)
    1.47  
    1.48 @@ -813,5 +820,3 @@
    1.49  by (asm_full_simp_tac (simpset() addsimps [real_of_nat_one RS sym,
    1.50  					   real_of_nat_add,Suc_diff_n]) 1);
    1.51  qed "real_of_nat_minus";
    1.52 -
    1.53 -