NEWS
changeset 22450 51ee032f9591
parent 22422 ee19cdb07528
child 22735 cf627add250a
equal deleted inserted replaced
22449:ece6952a8975 22450:51ee032f9591
   503 (trailing "_") by default; use '!' option for full details.
   503 (trailing "_") by default; use '!' option for full details.
   504 
   504 
   505 
   505 
   506 *** HOL ***
   506 *** HOL ***
   507 
   507 
   508 * Some steps towards more uniform lattice theory development in HOL.  Obvious changes:
   508 * Some steps towards more uniform lattice theory development in HOL.
   509 
   509 
   510     constants "meet" and "join" now named "inf" and "sup"
   510     constants "meet" and "join" now named "inf" and "sup"
   511     constant "Meet" now named "Inf"
   511     constant "Meet" now named "Inf"
   512 
   512 
   513   theorem renames:
   513     classes "meet_semilorder" and "join_semilorder" now named
       
   514       "lower_semilattice" and "upper_semilattice"
       
   515     class "lorder" now named "lattice"
       
   516     class "comp_lat" now named "complete_lattice"
       
   517 
       
   518     Instantiation of lattice classes allows explicit definitions
       
   519     for "inf" and "sup" operations.
       
   520 
       
   521   INCOMPATIBILITY. Theorem renames:
       
   522 
   514     meet_left_le            ~> inf_le1
   523     meet_left_le            ~> inf_le1
   515     meet_right_le           ~> inf_le2
   524     meet_right_le           ~> inf_le2
   516     join_left_le            ~> sup_ge1
   525     join_left_le            ~> sup_ge1
   517     join_right_le           ~> sup_ge2
   526     join_right_le           ~> sup_ge2
   518     meet_join_le            ~> inf_sup_ord
   527     meet_join_le            ~> inf_sup_ord
   601     Meet_lower              ~> Inf_lower
   610     Meet_lower              ~> Inf_lower
   602     Meet_set_def            ~> Inf_set_def
   611     Meet_set_def            ~> Inf_set_def
   603 
   612 
   604     listsp_meetI            ~> listsp_infI
   613     listsp_meetI            ~> listsp_infI
   605     listsp_meet_eq          ~> listsp_inf_eq
   614     listsp_meet_eq          ~> listsp_inf_eq
       
   615 
       
   616     meet_min                ~> inf_min
       
   617     join_max                ~> sup_max
   606 
   618 
   607 * Class (axclass + locale) "preorder" and "linear": facts "refl", "trans" and
   619 * Class (axclass + locale) "preorder" and "linear": facts "refl", "trans" and
   608 "cases" renamed ro "order_refl", "order_trans" and "linorder_cases", to
   620 "cases" renamed ro "order_refl", "order_trans" and "linorder_cases", to
   609 avoid clashes with HOL "refl" and "trans". INCOMPATIBILITY.
   621 avoid clashes with HOL "refl" and "trans". INCOMPATIBILITY.
   610 
   622