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