# HG changeset patch
# User wenzelm
# Date 1218207273 -7200
# Node ID 29ad1d91a5a3e20bfe8a0377f380eb1876bb111c
# Parent  e4a4d057749d3d76e4c1a44f9dc2a8734f2f4e2f
tuned formatting;

diff -r e4a4d057749d -r 29ad1d91a5a3 NEWS
--- a/NEWS	Fri Aug 08 15:36:40 2008 +0200
+++ b/NEWS	Fri Aug 08 16:54:33 2008 +0200
@@ -40,15 +40,17 @@
 
 *** 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
-has been generalized from nat to class semiring_div.  INCOMPATIBILITY.
-This involves the following theorem renames resulting from duplicate elimination:
+* 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 has been generalized from nat to class
+semiring_div.  INCOMPATIBILITY.  This involves the following theorem
+renames resulting from duplicate elimination:
 
     dvd_def_mod ~>          dvd_eq_mod_eq_0
     zero_dvd_iff ~>         dvd_0_left_iff
@@ -149,6 +151,7 @@
 one_zero ~> carrier_one_zero
 one_not_zero ~> carrier_one_not_zero  (collision with assumption)
 
+
 *** HOL-NSA ***
 
 * Created new image HOL-NSA, containing theories of nonstandard