author | wenzelm |

Fri Aug 08 16:54:33 2008 +0200 (2008-08-08 ago) | |

changeset 27793 | 29ad1d91a5a3 |

parent 27792 | e4a4d057749d |

child 27794 | bdea6e17cbe3 |

tuned formatting;

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