# HG changeset patch
# User paulson
# Date 927554098 -7200
# Node ID 70b251dc7055f6ea03ba09a0b5146b2979a98d13
# Parent  87c750df8888b4e685589c90e9a3c8b5daec8580
int_Suc->int_Suc_int_1 avoiding confusion with the more useful Bin.int_Suc

diff -r 87c750df8888 -r 70b251dc7055 src/HOL/Integ/Int.ML
--- a/src/HOL/Integ/Int.ML	Mon May 24 15:54:12 1999 +0200
+++ b/src/HOL/Integ/Int.ML	Mon May 24 15:54:58 1999 +0200
@@ -24,12 +24,12 @@
 Goal "(w < z + int (Suc m)) = (w < z + int m | w = z + int m)";
 by (auto_tac (claset(),
 	      simpset() addsimps [zless_iff_Suc_zadd, zadd_assoc, zadd_int]));
-by (cut_inst_tac [("m","m")] int_Suc 1);
-by (cut_inst_tac [("m","n")] int_Suc 1);
+by (cut_inst_tac [("m","m")] int_Suc_int_1 1);
+by (cut_inst_tac [("m","n")] int_Suc_int_1 1);
 by (Asm_full_simp_tac 1);
 by (exhaust_tac "n" 1);
 by Auto_tac;
-by (cut_inst_tac [("m","m")] int_Suc 1);
+by (cut_inst_tac [("m","m")] int_Suc_int_1 1);
 by (full_simp_tac (simpset() addsimps zadd_ac) 1);
 by (asm_full_simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1);
 by (auto_tac (claset(),
diff -r 87c750df8888 -r 70b251dc7055 src/HOL/Integ/IntDef.ML
--- a/src/HOL/Integ/IntDef.ML	Mon May 24 15:54:12 1999 +0200
+++ b/src/HOL/Integ/IntDef.ML	Mon May 24 15:54:58 1999 +0200
@@ -220,7 +220,7 @@
 
 Goal "int (Suc m) = int 1 + (int m)";
 by (simp_tac (simpset() addsimps [zadd_int]) 1);
-qed "int_Suc";
+qed "int_Suc_int_1";
 
 Goalw [int_def] "int 0 + z = z";
 by (res_inst_tac [("z","z")] eq_Abs_Integ 1);