# HG changeset patch
# User paulson
# Date 959099291 -7200
# Node ID 6aad5381ba83a4681d9ce2c535e41ab363a2f303
# Parent  df06883c1dcf47858d29e9e1b71697f0b6f24228
added type constraint ::nat because 0 is now overloaded

diff -r df06883c1dcf -r 6aad5381ba83 src/HOL/Nat.ML
--- a/src/HOL/Nat.ML	Tue May 23 18:24:48 2000 +0200
+++ b/src/HOL/Nat.ML	Tue May 23 18:28:11 2000 +0200
@@ -26,18 +26,18 @@
 by (REPEAT (Blast_tac 1));
 qed "not0_implies_Suc";
 
-Goal "m<n ==> n ~= 0";
+Goal "!!n::nat. m<n ==> n ~= 0";
 by (case_tac "n" 1);
 by (ALLGOALS Asm_full_simp_tac);
 qed "gr_implies_not0";
 
-Goal "(n ~= 0) = (0 < n)";
+Goal "!!n::nat. (n ~= 0) = (0 < n)";
 by (case_tac "n" 1);
 by Auto_tac;
 qed "neq0_conv";
 AddIffs [neq0_conv];
 
-Goal "(0 ~= n) = (0 < n)";
+Goal "!!n::nat. (0 ~= n) = (0 < n)";
 by (case_tac "n" 1);
 by Auto_tac;
 qed "zero_neq_conv";
@@ -50,7 +50,7 @@
 by(fast_tac (claset() addIs [not0_implies_Suc]) 1);
 qed "gr0_conv_Suc";
 
-Goal "(~(0 < n)) = (n=0)";
+Goal "!!n::nat. (~(0 < n)) = (n=0)";
 by (rtac iffI 1);
  by (etac swap 1);
  by (ALLGOALS Asm_full_simp_tac);
@@ -95,12 +95,12 @@
 by (ALLGOALS (blast_tac (claset() addIs prems@[less_trans])));
 qed "nat_induct2";
 
-Goal "min 0 n = 0";
+Goal "min 0 n = (0::nat)";
 by (rtac min_leastL 1);
 by (Simp_tac 1);
 qed "min_0L";
 
-Goal "min n 0 = 0";
+Goal "min n 0 = (0::nat)";
 by (rtac min_leastR 1);
 by (Simp_tac 1);
 qed "min_0R";
@@ -111,11 +111,11 @@
 
 Addsimps [min_0L,min_0R,min_Suc_Suc];
 
-Goalw [max_def] "max 0 n = n";
+Goalw [max_def] "max 0 n = (n::nat)";
 by (Simp_tac 1);
 qed "max_0L";
 
-Goalw [max_def] "max n 0 = n";
+Goalw [max_def] "max n 0 = (n::nat)";
 by (Simp_tac 1);
 qed "max_0R";
 
diff -r df06883c1dcf -r 6aad5381ba83 src/HOL/NatDef.ML
--- a/src/HOL/NatDef.ML	Tue May 23 18:24:48 2000 +0200
+++ b/src/HOL/NatDef.ML	Tue May 23 18:28:11 2000 +0200
@@ -184,13 +184,9 @@
                   eresolve_tac (prems@[asm_rl, Pair_inject])));
 qed "lessE";
 
-Goal "~ n<0";
-by (rtac notI 1);
-by (etac lessE 1);
-by (etac Zero_neq_Suc 1);
-by (etac Zero_neq_Suc 1);
+Goal "~ n < (0::nat)";
+by (blast_tac (claset() addEs [lessE]) 1);
 qed "not_less0";
-
 AddIffs [not_less0];
 
 (* n<0 ==> R *)
@@ -312,7 +308,7 @@
 (*  m<=n ==> m < Suc n  *)
 bind_thm ("le_imp_less_Suc", less_Suc_eq_le RS iffD2);
 
-Goalw [le_def] "0 <= n";
+Goalw [le_def] "(0::nat) <= n";
 by (rtac not_less0 1);
 qed "le0";
 AddIffs [le0];
@@ -321,7 +317,7 @@
 by (Simp_tac 1);
 qed "Suc_n_not_le_n";
 
-Goalw [le_def] "(i <= 0) = (i = 0)";
+Goalw [le_def] "!!i::nat. (i <= 0) = (i = 0)";
 by (nat_ind_tac "i" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "le_0_eq";