src/HOL/Nat.ML
changeset 8942 6aad5381ba83
parent 8442 96023903c2df
child 9108 9fff97d29837
     1.1 --- a/src/HOL/Nat.ML	Tue May 23 18:24:48 2000 +0200
     1.2 +++ b/src/HOL/Nat.ML	Tue May 23 18:28:11 2000 +0200
     1.3 @@ -26,18 +26,18 @@
     1.4  by (REPEAT (Blast_tac 1));
     1.5  qed "not0_implies_Suc";
     1.6  
     1.7 -Goal "m<n ==> n ~= 0";
     1.8 +Goal "!!n::nat. m<n ==> n ~= 0";
     1.9  by (case_tac "n" 1);
    1.10  by (ALLGOALS Asm_full_simp_tac);
    1.11  qed "gr_implies_not0";
    1.12  
    1.13 -Goal "(n ~= 0) = (0 < n)";
    1.14 +Goal "!!n::nat. (n ~= 0) = (0 < n)";
    1.15  by (case_tac "n" 1);
    1.16  by Auto_tac;
    1.17  qed "neq0_conv";
    1.18  AddIffs [neq0_conv];
    1.19  
    1.20 -Goal "(0 ~= n) = (0 < n)";
    1.21 +Goal "!!n::nat. (0 ~= n) = (0 < n)";
    1.22  by (case_tac "n" 1);
    1.23  by Auto_tac;
    1.24  qed "zero_neq_conv";
    1.25 @@ -50,7 +50,7 @@
    1.26  by(fast_tac (claset() addIs [not0_implies_Suc]) 1);
    1.27  qed "gr0_conv_Suc";
    1.28  
    1.29 -Goal "(~(0 < n)) = (n=0)";
    1.30 +Goal "!!n::nat. (~(0 < n)) = (n=0)";
    1.31  by (rtac iffI 1);
    1.32   by (etac swap 1);
    1.33   by (ALLGOALS Asm_full_simp_tac);
    1.34 @@ -95,12 +95,12 @@
    1.35  by (ALLGOALS (blast_tac (claset() addIs prems@[less_trans])));
    1.36  qed "nat_induct2";
    1.37  
    1.38 -Goal "min 0 n = 0";
    1.39 +Goal "min 0 n = (0::nat)";
    1.40  by (rtac min_leastL 1);
    1.41  by (Simp_tac 1);
    1.42  qed "min_0L";
    1.43  
    1.44 -Goal "min n 0 = 0";
    1.45 +Goal "min n 0 = (0::nat)";
    1.46  by (rtac min_leastR 1);
    1.47  by (Simp_tac 1);
    1.48  qed "min_0R";
    1.49 @@ -111,11 +111,11 @@
    1.50  
    1.51  Addsimps [min_0L,min_0R,min_Suc_Suc];
    1.52  
    1.53 -Goalw [max_def] "max 0 n = n";
    1.54 +Goalw [max_def] "max 0 n = (n::nat)";
    1.55  by (Simp_tac 1);
    1.56  qed "max_0L";
    1.57  
    1.58 -Goalw [max_def] "max n 0 = n";
    1.59 +Goalw [max_def] "max n 0 = (n::nat)";
    1.60  by (Simp_tac 1);
    1.61  qed "max_0R";
    1.62