# HG changeset patch
# User haftmann
# Date 1174077126 -3600
# Node ID 51ee032f959190e69d5482b2025332ce483b69b2
# Parent  ece6952a89759d40a697a1e638e45df3e61a8a4b
lattice cleanup

diff -r ece6952a8975 -r 51ee032f9591 NEWS
--- 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.