src/HOL/Nat.ML
changeset 7089 9bfb8e218b99
parent 7058 8dfea70eb6b7
child 8115 c802042066e8
     1.1 --- a/src/HOL/Nat.ML	Tue Jul 27 10:30:26 1999 +0200
     1.2 +++ b/src/HOL/Nat.ML	Tue Jul 27 17:19:31 1999 +0200
     1.3 @@ -33,14 +33,13 @@
     1.4  
     1.5  Goal "(n ~= 0) = (0 < n)";
     1.6  by (exhaust_tac "n" 1);
     1.7 -by (Blast_tac 1);
     1.8 -by (Blast_tac 1);
     1.9 +by Auto_tac;
    1.10  qed "neq0_conv";
    1.11  AddIffs [neq0_conv];
    1.12  
    1.13  Goal "(0 ~= n) = (0 < n)";
    1.14  by (exhaust_tac "n" 1);
    1.15 -by (Auto_tac);
    1.16 +by Auto_tac;
    1.17  qed "zero_neq_conv";
    1.18  AddIffs [zero_neq_conv];
    1.19  
    1.20 @@ -75,33 +74,16 @@
    1.21  by (hyp_subst_tac 1);
    1.22  by (rewtac Least_nat_def);
    1.23  by (rtac (select_equality RS arg_cong RS sym) 1);
    1.24 -by (Safe_tac);
    1.25 -by (dtac Suc_mono 1);
    1.26 -by (Blast_tac 1);
    1.27 -by (cut_facts_tac [less_linear] 1);
    1.28 -by (Safe_tac);
    1.29 -by (atac 2);
    1.30 -by (Blast_tac 2);
    1.31 -by (dtac Suc_mono 1);
    1.32 -by (Blast_tac 1);
    1.33 +by (blast_tac (claset() addDs [Suc_mono]) 1);
    1.34 +by (cut_inst_tac [("m","m")] less_linear 1);
    1.35 +by (blast_tac (claset() addIs [Suc_mono]) 1);
    1.36  qed "Least_Suc";
    1.37  
    1.38  val prems = Goal "[| P 0; P 1; !!k. P k ==> P (Suc (Suc k)) |] ==> P n";
    1.39 -by (cut_facts_tac prems 1);
    1.40  by (rtac less_induct 1);
    1.41  by (exhaust_tac "n" 1);
    1.42 -by (hyp_subst_tac 1);
    1.43 -by (atac 1);
    1.44 -by (hyp_subst_tac 1);
    1.45 -by (exhaust_tac "nat" 1);
    1.46 -by (hyp_subst_tac 1);
    1.47 -by (atac 1);
    1.48 -by (hyp_subst_tac 1);
    1.49 -by (resolve_tac prems 1);
    1.50 -by (dtac spec 1);
    1.51 -by (etac mp 1);
    1.52 -by (rtac (lessI RS less_trans) 1);
    1.53 -by (rtac (lessI RS Suc_mono) 1);
    1.54 +by (exhaust_tac "nat" 2);
    1.55 +by (ALLGOALS (blast_tac (claset() addIs prems@[less_trans])));
    1.56  qed "nat_induct2";
    1.57  
    1.58  Goal "min 0 n = 0";