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