summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Fri, 08 Aug 2008 16:54:33 +0200 | |

changeset 27793 | 29ad1d91a5a3 |

parent 27792 | e4a4d057749d |

child 27794 | bdea6e17cbe3 |

tuned formatting;

--- 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