--- a/NEWS Fri Jul 25 12:03:31 2008 +0200
+++ b/NEWS Fri Jul 25 12:03:32 2008 +0200
@@ -19,6 +19,8 @@
*** Pure ***
+* dropped "locale (open)". INCOMPATBILITY.
+
* Command 'instance': attached definitions no longer accepted.
INCOMPATIBILITY, use proper 'instantiation' target.
@@ -34,6 +36,10 @@
*** HOL ***
+* 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 preorder_class.*.
+
* HOL/Ring_and_Field and HOL/Divides: Definition of "op dvd" has been moved
to separate class dvd in Ring_and_Field; a couple of lemmas on dvd has been
generalized to class comm_semiring_1. Likewise a bunch of lemmas from Divides