--- a/src/HOL/Integ/IntDef.ML Tue Jul 13 10:44:13 1999 +0200
+++ b/src/HOL/Integ/IntDef.ML Tue Jul 13 10:44:45 1999 +0200
@@ -93,7 +93,7 @@
by (Fast_tac 1);
by Safe_tac;
by (Asm_full_simp_tac 1);
-qed "inj_nat";
+qed "inj_int";
(**** zminus: unary negation on Integ ****)
@@ -473,7 +473,7 @@
bind_thm("int_neqE", int_neq_iff RS iffD1 RS disjE);
Goal "(int m = int n) = (m = n)";
-by (fast_tac (claset() addSEs [inj_nat RS injD]) 1);
+by (fast_tac (claset() addSEs [inj_int RS injD]) 1);
qed "int_int_eq";
AddIffs [int_int_eq];