src/HOL/Nat.ML
changeset 8442 96023903c2df
parent 8423 3c19160b6432
child 8942 6aad5381ba83
     1.1 --- a/src/HOL/Nat.ML	Mon Mar 13 15:42:19 2000 +0100
     1.2 +++ b/src/HOL/Nat.ML	Mon Mar 13 16:23:34 2000 +0100
     1.3 @@ -22,23 +22,23 @@
     1.4  val [nat_case_0, nat_case_Suc] = nat.cases;
     1.5  
     1.6  Goal "n ~= 0 ==> EX m. n = Suc m";
     1.7 -by (cases_tac "n" 1);
     1.8 +by (case_tac "n" 1);
     1.9  by (REPEAT (Blast_tac 1));
    1.10  qed "not0_implies_Suc";
    1.11  
    1.12  Goal "m<n ==> n ~= 0";
    1.13 -by (cases_tac "n" 1);
    1.14 +by (case_tac "n" 1);
    1.15  by (ALLGOALS Asm_full_simp_tac);
    1.16  qed "gr_implies_not0";
    1.17  
    1.18  Goal "(n ~= 0) = (0 < n)";
    1.19 -by (cases_tac "n" 1);
    1.20 +by (case_tac "n" 1);
    1.21  by Auto_tac;
    1.22  qed "neq0_conv";
    1.23  AddIffs [neq0_conv];
    1.24  
    1.25  Goal "(0 ~= n) = (0 < n)";
    1.26 -by (cases_tac "n" 1);
    1.27 +by (case_tac "n" 1);
    1.28  by Auto_tac;
    1.29  qed "zero_neq_conv";
    1.30  AddIffs [zero_neq_conv];
    1.31 @@ -64,7 +64,7 @@
    1.32  
    1.33  (*Useful in certain inductive arguments*)
    1.34  Goal "(m < Suc n) = (m=0 | (EX j. m = Suc j & j < n))";
    1.35 -by (cases_tac "m" 1);
    1.36 +by (case_tac "m" 1);
    1.37  by Auto_tac;
    1.38  qed "less_Suc_eq_0_disj";
    1.39  
    1.40 @@ -74,11 +74,11 @@
    1.41  by (fold_goals_tac [Least_nat_def]);
    1.42  by (safe_tac (claset() addSEs [LeastI]));
    1.43  by (rename_tac "j" 1);
    1.44 -by (cases_tac "j" 1);
    1.45 +by (case_tac "j" 1);
    1.46  by (Blast_tac 1);
    1.47  by (blast_tac (claset() addDs [Suc_less_SucD, not_less_Least]) 1);
    1.48  by (rename_tac "k n" 1);
    1.49 -by (cases_tac "k" 1);
    1.50 +by (case_tac "k" 1);
    1.51  by (Blast_tac 1);
    1.52  by (hyp_subst_tac 1);
    1.53  by (rewtac Least_nat_def);
    1.54 @@ -90,8 +90,8 @@
    1.55  
    1.56  val prems = Goal "[| P 0; P 1; !!k. P k ==> P (Suc (Suc k)) |] ==> P n";
    1.57  by (rtac less_induct 1);
    1.58 -by (cases_tac "n" 1);
    1.59 -by (cases_tac "nat" 2);
    1.60 +by (case_tac "n" 1);
    1.61 +by (case_tac "nat" 2);
    1.62  by (ALLGOALS (blast_tac (claset() addIs prems@[less_trans])));
    1.63  qed "nat_induct2";
    1.64