# HG changeset patch
# User nipkow
# Date 900415801 -7200
# Node ID 216a5dab14b68de2cb4b6239701c28269f10936b
# Parent  013ea0f023e30db39e108ae068c705db179943bb
inj_on

diff -r 013ea0f023e3 -r 216a5dab14b6 NEWS
--- a/NEWS	Tue Jul 14 13:29:39 1998 +0200
+++ b/NEWS	Tue Jul 14 13:30:01 1998 +0200
@@ -8,7 +8,7 @@
 *** Overview of INCOMPATIBILITIES (see below for more details) ***
 
 * HOL/inductive requires Inductive.thy as an ancestor;
-
+* `inj_onto' is now called `inj_on' (which makes more sense)
 
 *** Proof tools ***