NEWS
changeset 15677 8770edbf8f28
parent 15570 8d8c70b41bab
child 15696 1da4ce092c0b
     1.1 --- a/NEWS	Thu Apr 07 13:29:41 2005 +0200
     1.2 +++ b/NEWS	Thu Apr 07 14:07:40 2005 +0200
     1.3 @@ -514,6 +514,9 @@
     1.4    also an x-symbol version with subscripts "\<Union>\<^bsub>i <= n\<^esub>. A"
     1.5    like in normal math, and corresponding versions for < and for intersection.
     1.6  
     1.7 +* HOL/List: Ordering "lexico" is renamed "lenlex" and the standard
     1.8 +  lexicographic dictonary ordering has been added as "lexord".
     1.9 +
    1.10  * ML: the legacy theory structures Int and List have been removed. They had
    1.11    conflicted with ML Basis Library structures having the same names.
    1.12