lattice cleanup
authorhaftmann
Fri Mar 16 21:32:06 2007 +0100 (2007-03-16)
changeset 2245051ee032f9591
parent 22449 ece6952a8975
child 22451 989182f660e0
lattice cleanup
NEWS
     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.