--- a/NEWS Fri Mar 16 21:32:05 2007 +0100
+++ b/NEWS Fri Mar 16 21:32:06 2007 +0100
@@ -505,12 +505,21 @@
*** HOL ***
-* Some steps towards more uniform lattice theory development in HOL. Obvious changes:
+* Some steps towards more uniform lattice theory development in HOL.
constants "meet" and "join" now named "inf" and "sup"
constant "Meet" now named "Inf"
- theorem renames:
+ classes "meet_semilorder" and "join_semilorder" now named
+ "lower_semilattice" and "upper_semilattice"
+ class "lorder" now named "lattice"
+ class "comp_lat" now named "complete_lattice"
+
+ Instantiation of lattice classes allows explicit definitions
+ for "inf" and "sup" operations.
+
+ INCOMPATIBILITY. Theorem renames:
+
meet_left_le ~> inf_le1
meet_right_le ~> inf_le2
join_left_le ~> sup_ge1
@@ -604,6 +613,9 @@
listsp_meetI ~> listsp_infI
listsp_meet_eq ~> listsp_inf_eq
+ meet_min ~> inf_min
+ join_max ~> sup_max
+
* Class (axclass + locale) "preorder" and "linear": facts "refl", "trans" and
"cases" renamed ro "order_refl", "order_trans" and "linorder_cases", to
avoid clashes with HOL "refl" and "trans". INCOMPATIBILITY.