inj_on
authornipkow
Tue Jul 14 13:30:01 1998 +0200 (1998-07-14)
changeset 5140216a5dab14b6
parent 5139 013ea0f023e3
child 5141 495a4f9af897
inj_on
NEWS
     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