1.1 --- a/NEWS	Sun Aug 10 12:38:26 2008 +0200
     1.2 +++ b/NEWS	Mon Aug 11 14:49:53 2008 +0200
     1.3 @@ -40,6 +40,10 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* HOL/Orderings: class "wellorder" moved here, with explicit induction rule
     1.8 +"less_induct" as assumption.  For instantiation of "wellorder" by means
     1.9 +of predicate "wf", use rule wf_wellorderI.  INCOMPATIBILITY.
    1.10 +
    1.11  * HOL/Orderings: added class "preorder" as superclass of "order".
    1.12  INCOMPATIBILITY: Instantiation proofs for order, linorder
    1.13  etc. slightly changed.  Some theorems named order_class.* now named
    1.14 @@ -5671,4 +5675,5 @@
    1.15  
    1.16  :mode=text:wrap=hard:maxLineLen=72:
    1.17  
    1.18 +
    1.19  $Id$