NEWS
changeset 10428 8f15fbce549f
parent 10421 ceaab640734b
child 10452 abeefb0a79ae
     1.1 --- a/NEWS	Fri Nov 10 16:26:44 2000 +0100
     1.2 +++ b/NEWS	Fri Nov 10 16:31:28 2000 +0100
     1.3 @@ -57,6 +57,9 @@
     1.4  HOL/Induct/Multiset, HOL/Induct/Acc (as Accessible_Part), HOL/While
     1.5  (as While_Combinator), HOL/Lex/Prefix (as List_Prefix);
     1.6  
     1.7 +* >, >= and \<ge> can now be used for input; they are immediately replaced
     1.8 +  by the converse symbol, eg "x > y" by "y < x".
     1.9 +
    1.10  * HOL/typedef: simplified package, provide more useful rules (see also
    1.11  HOL/subset.thy);
    1.12