src/HOL/NatDef.ML
changeset 3023 01364e2f30ad
parent 2935 998cb95fdd43
child 3040 7d48671753da
     1.1 --- a/src/HOL/NatDef.ML	Wed Apr 23 11:12:10 1997 +0200
     1.2 +++ b/src/HOL/NatDef.ML	Wed Apr 23 11:18:29 1997 +0200
     1.3 @@ -377,21 +377,21 @@
     1.4  
     1.5  qed_goal "nat_induct2" thy 
     1.6  "[| P 0; P 1; !!k. P k ==> P (Suc (Suc k)) |] ==> P n" (fn prems => [
     1.7 -	cut_facts_tac prems 1,
     1.8 -	rtac less_induct 1,
     1.9 -	res_inst_tac [("n","n")] natE 1,
    1.10 -	 hyp_subst_tac 1,
    1.11 -	 atac 1,
    1.12 -	hyp_subst_tac 1,
    1.13 -	res_inst_tac [("n","x")] natE 1,
    1.14 -	 hyp_subst_tac 1,
    1.15 -	 atac 1,
    1.16 -	hyp_subst_tac 1,
    1.17 -	resolve_tac prems 1,
    1.18 -	dtac spec 1,
    1.19 -	etac mp 1,
    1.20 -	rtac (lessI RS less_trans) 1,
    1.21 -	rtac (lessI RS Suc_mono) 1]);
    1.22 +        cut_facts_tac prems 1,
    1.23 +        rtac less_induct 1,
    1.24 +        res_inst_tac [("n","n")] natE 1,
    1.25 +         hyp_subst_tac 1,
    1.26 +         atac 1,
    1.27 +        hyp_subst_tac 1,
    1.28 +        res_inst_tac [("n","x")] natE 1,
    1.29 +         hyp_subst_tac 1,
    1.30 +         atac 1,
    1.31 +        hyp_subst_tac 1,
    1.32 +        resolve_tac prems 1,
    1.33 +        dtac spec 1,
    1.34 +        etac mp 1,
    1.35 +        rtac (lessI RS less_trans) 1,
    1.36 +        rtac (lessI RS Suc_mono) 1]);
    1.37  
    1.38  (*** Properties of <= ***)
    1.39  
    1.40 @@ -521,15 +521,15 @@
    1.41  
    1.42  goal thy "!!i. [| i <= j; j <= k |] ==> i <= (k::nat)";
    1.43  by (EVERY1[dtac le_imp_less_or_eq, 
    1.44 -	   dtac le_imp_less_or_eq,
    1.45 -	   rtac less_or_eq_imp_le, 
    1.46 -	   blast_tac (!claset addIs [less_trans])]);
    1.47 +           dtac le_imp_less_or_eq,
    1.48 +           rtac less_or_eq_imp_le, 
    1.49 +           blast_tac (!claset addIs [less_trans])]);
    1.50  qed "le_trans";
    1.51  
    1.52  goal thy "!!m. [| m <= n; n <= m |] ==> m = (n::nat)";
    1.53  by (EVERY1[dtac le_imp_less_or_eq, 
    1.54 -	   dtac le_imp_less_or_eq,
    1.55 -	   blast_tac (!claset addEs [less_irrefl,less_asym])]);
    1.56 +           dtac le_imp_less_or_eq,
    1.57 +           blast_tac (!claset addEs [less_irrefl,less_asym])]);
    1.58  qed "le_anti_sym";
    1.59  
    1.60  goal thy "(Suc(n) <= Suc(m)) = (n <= m)";
    1.61 @@ -540,11 +540,11 @@
    1.62  
    1.63  (* Axiom 'order_le_less' of class 'order': *)
    1.64  goal thy "(m::nat) < n = (m <= n & m ~= n)";
    1.65 -br iffI 1;
    1.66 - br conjI 1;
    1.67 -  be less_imp_le 1;
    1.68 - be (less_not_refl2 RS not_sym) 1;
    1.69 -by(blast_tac (!claset addSDs [le_imp_less_or_eq]) 1);
    1.70 +by (rtac iffI 1);
    1.71 + by (rtac conjI 1);
    1.72 +  by (etac less_imp_le 1);
    1.73 + by (etac (less_not_refl2 RS not_sym) 1);
    1.74 +by (blast_tac (!claset addSDs [le_imp_less_or_eq]) 1);
    1.75  qed "nat_less_le";
    1.76  
    1.77  (** LEAST -- the least number operator **)