NEWS
changeset 5140 216a5dab14b6
parent 5131 dd4ac220b8b4
child 5142 c56aa8b59dc0
     1.1 --- a/NEWS	Tue Jul 14 13:29:39 1998 +0200
     1.2 +++ b/NEWS	Tue Jul 14 13:30:01 1998 +0200
     1.3 @@ -8,7 +8,7 @@
     1.4  *** Overview of INCOMPATIBILITIES (see below for more details) ***
     1.5  
     1.6  * HOL/inductive requires Inductive.thy as an ancestor;
     1.7 -
     1.8 +* `inj_onto' is now called `inj_on' (which makes more sense)
     1.9  
    1.10  *** Proof tools ***
    1.11