# HG changeset patch
# User paulson
# Date 931855485 -7200
# Node ID 500038b6063b18115bcd3aeb4c4c6ee635c25094
# Parent  cac1e4e9c821780bb93d7006bcc0a54afc1aa2f6
renamed inj_nat to inj_int

diff -r cac1e4e9c821 -r 500038b6063b src/HOL/Integ/IntDef.ML
--- 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];