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

author | ballarin |

Tue, 29 Jul 2008 16:14:56 +0200 | |

changeset 27696 | 15b65db66751 |

parent 27695 | 033732c90ebd |

child 27697 | bcf941cc3324 |

Unit_inv_l, Unit_inv_r made [simp];
Renamed theorems;
New theory on divisibility.

--- a/NEWS Tue Jul 29 14:20:22 2008 +0200 +++ b/NEWS Tue Jul 29 16:14:56 2008 +0200 @@ -123,6 +123,22 @@ theorems. Changes in simp rules. INCOMPATIBILITY. +*** HOL-Algebra *** + +* Units_l_inv and Units_r_inv are now simprules by default. +INCOMPATIBILITY. Simplifier proof that require deletion of l_inv +and/or r_inv will now also require deletion of these lemmas. + +* Renamed the following theorems. INCOMPATIBILITY. +UpperD ~> Upper_memD +LowerD ~> Lower_memD +least_carrier ~> least_closed +greatest_carrier ~> greatest_closed +greatest_Lower_above ~> greatest_Lower_below + +* New theory of factorial domains. + + *** HOL-NSA *** * Created new image HOL-NSA, containing theories of nonstandard