tuned formatting;
authorwenzelm
Fri Aug 08 16:54:33 2008 +0200 (2008-08-08 ago)
changeset 2779329ad1d91a5a3
parent 27792 e4a4d057749d
child 27794 bdea6e17cbe3
tuned formatting;
NEWS
     1.1 --- a/NEWS	Fri Aug 08 15:36:40 2008 +0200
     1.2 +++ b/NEWS	Fri Aug 08 16:54:33 2008 +0200
     1.3 @@ -40,15 +40,17 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 -* HOL/Orderings: added class "preorder" as superclass of "order".  INCOMPATIBILITY:
     1.8 -Instantiation proofs for order, linorder etc. slightly changed.  Some theorems
     1.9 -named order_class.* now named preorder_class.*.
    1.10 -
    1.11 -* HOL/Ring_and_Field and HOL/Divides: Definition of "op dvd" has been moved
    1.12 -to separate class dvd in Ring_and_Field;  a couple of lemmas on dvd has been
    1.13 -generalized to class comm_semiring_1.  Likewise a bunch of lemmas from Divides
    1.14 -has been generalized from nat to class semiring_div.  INCOMPATIBILITY.
    1.15 -This involves the following theorem renames resulting from duplicate elimination:
    1.16 +* HOL/Orderings: added class "preorder" as superclass of "order".
    1.17 +INCOMPATIBILITY: Instantiation proofs for order, linorder
    1.18 +etc. slightly changed.  Some theorems named order_class.* now named
    1.19 +preorder_class.*.
    1.20 +
    1.21 +* HOL/Ring_and_Field and HOL/Divides: Definition of "op dvd" has been
    1.22 +moved to separate class dvd in Ring_and_Field; a couple of lemmas on
    1.23 +dvd has been generalized to class comm_semiring_1.  Likewise a bunch
    1.24 +of lemmas from Divides has been generalized from nat to class
    1.25 +semiring_div.  INCOMPATIBILITY.  This involves the following theorem
    1.26 +renames resulting from duplicate elimination:
    1.27  
    1.28      dvd_def_mod ~>          dvd_eq_mod_eq_0
    1.29      zero_dvd_iff ~>         dvd_0_left_iff
    1.30 @@ -149,6 +151,7 @@
    1.31  one_zero ~> carrier_one_zero
    1.32  one_not_zero ~> carrier_one_not_zero  (collision with assumption)
    1.33  
    1.34 +
    1.35  *** HOL-NSA ***
    1.36  
    1.37  * Created new image HOL-NSA, containing theories of nonstandard