inj

--- a/NEWS	Wed Feb 03 14:02:49 1999 +0100
+++ b/NEWS	Wed Feb 03 15:48:52 1999 +0100
@@ -8,6 +8,8 @@
 
 * HOL: Removed the obsolete syntax "Compl A"; use -A for set complement
 
+* HOL: the predicate "inj" is now defined by translation to "inj_on"
+
 * ZF: The con_defs part of an inductive definition may no longer refer to 
   constants declared in the same theory;