summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

NEWS

changeset 22450 | 51ee032f9591 |

parent 22422 | ee19cdb07528 |

child 22735 | cf627add250a |

1.1 --- a/NEWS Fri Mar 16 21:32:05 2007 +0100 1.2 +++ b/NEWS Fri Mar 16 21:32:06 2007 +0100 1.3 @@ -505,12 +505,21 @@ 1.4 1.5 *** HOL *** 1.6 1.7 -* Some steps towards more uniform lattice theory development in HOL. Obvious changes: 1.8 +* Some steps towards more uniform lattice theory development in HOL. 1.9 1.10 constants "meet" and "join" now named "inf" and "sup" 1.11 constant "Meet" now named "Inf" 1.12 1.13 - theorem renames: 1.14 + classes "meet_semilorder" and "join_semilorder" now named 1.15 + "lower_semilattice" and "upper_semilattice" 1.16 + class "lorder" now named "lattice" 1.17 + class "comp_lat" now named "complete_lattice" 1.18 + 1.19 + Instantiation of lattice classes allows explicit definitions 1.20 + for "inf" and "sup" operations. 1.21 + 1.22 + INCOMPATIBILITY. Theorem renames: 1.23 + 1.24 meet_left_le ~> inf_le1 1.25 meet_right_le ~> inf_le2 1.26 join_left_le ~> sup_ge1 1.27 @@ -604,6 +613,9 @@ 1.28 listsp_meetI ~> listsp_infI 1.29 listsp_meet_eq ~> listsp_inf_eq 1.30 1.31 + meet_min ~> inf_min 1.32 + join_max ~> sup_max 1.33 + 1.34 * Class (axclass + locale) "preorder" and "linear": facts "refl", "trans" and 1.35 "cases" renamed ro "order_refl", "order_trans" and "linorder_cases", to 1.36 avoid clashes with HOL "refl" and "trans". INCOMPATIBILITY.