NEWS
changeset 22422 ee19cdb07528
parent 22384 33a46e6c7f04
child 22450 51ee032f9591
     1.1 --- a/NEWS	Tue Mar 06 16:40:32 2007 +0100
     1.2 +++ b/NEWS	Fri Mar 09 08:45:50 2007 +0100
     1.3 @@ -505,6 +505,105 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Some steps towards more uniform lattice theory development in HOL.  Obvious changes:
     1.8 +
     1.9 +    constants "meet" and "join" now named "inf" and "sup"
    1.10 +    constant "Meet" now named "Inf"
    1.11 +
    1.12 +  theorem renames:
    1.13 +    meet_left_le            ~> inf_le1
    1.14 +    meet_right_le           ~> inf_le2
    1.15 +    join_left_le            ~> sup_ge1
    1.16 +    join_right_le           ~> sup_ge2
    1.17 +    meet_join_le            ~> inf_sup_ord
    1.18 +    le_meetI                ~> le_infI
    1.19 +    join_leI                ~> le_supI
    1.20 +    le_meet                 ~> le_inf_iff
    1.21 +    le_join                 ~> ge_sup_conv
    1.22 +    meet_idempotent         ~> inf_idem
    1.23 +    join_idempotent         ~> sup_idem
    1.24 +    meet_comm               ~> inf_commute
    1.25 +    join_comm               ~> sup_commute
    1.26 +    meet_leI1               ~> le_infI1
    1.27 +    meet_leI2               ~> le_infI2
    1.28 +    le_joinI1               ~> le_supI1
    1.29 +    le_joinI2               ~> le_supI2
    1.30 +    meet_assoc              ~> inf_assoc
    1.31 +    join_assoc              ~> sup_assoc
    1.32 +    meet_left_comm          ~> inf_left_commute
    1.33 +    meet_left_idempotent    ~> inf_left_idem
    1.34 +    join_left_comm          ~> sup_left_commute
    1.35 +    join_left_idempotent    ~> sup_left_idem
    1.36 +    meet_aci                ~> inf_aci
    1.37 +    join_aci                ~> sup_aci
    1.38 +    le_def_meet             ~> le_iff_inf
    1.39 +    le_def_join             ~> le_iff_sup
    1.40 +    join_absorp2            ~> sup_absorb2
    1.41 +    join_absorp1            ~> sup_absorb1
    1.42 +    meet_absorp1            ~> inf_absorb1
    1.43 +    meet_absorp2            ~> inf_absorb2
    1.44 +    meet_join_absorp        ~> inf_sup_absorb
    1.45 +    join_meet_absorp        ~> sup_inf_absorb
    1.46 +    distrib_join_le         ~> distrib_sup_le
    1.47 +    distrib_meet_le         ~> distrib_inf_le
    1.48 +
    1.49 +    add_meet_distrib_left   ~> add_inf_distrib_left
    1.50 +    add_join_distrib_left   ~> add_sup_distrib_left
    1.51 +    is_join_neg_meet        ~> is_join_neg_inf
    1.52 +    is_meet_neg_join        ~> is_meet_neg_sup
    1.53 +    add_meet_distrib_right  ~> add_inf_distrib_right
    1.54 +    add_join_distrib_right  ~> add_sup_distrib_right
    1.55 +    add_meet_join_distribs  ~> add_sup_inf_distribs
    1.56 +    join_eq_neg_meet        ~> sup_eq_neg_inf
    1.57 +    meet_eq_neg_join        ~> inf_eq_neg_sup
    1.58 +    add_eq_meet_join        ~> add_eq_inf_sup
    1.59 +    meet_0_imp_0            ~> inf_0_imp_0
    1.60 +    join_0_imp_0            ~> sup_0_imp_0
    1.61 +    meet_0_eq_0             ~> inf_0_eq_0
    1.62 +    join_0_eq_0             ~> sup_0_eq_0
    1.63 +    neg_meet_eq_join        ~> neg_inf_eq_sup
    1.64 +    neg_join_eq_meet        ~> neg_sup_eq_inf
    1.65 +    join_eq_if              ~> sup_eq_if
    1.66 +
    1.67 +    mono_meet               ~> mono_inf
    1.68 +    mono_join               ~> mono_sup
    1.69 +    meet_bool_eq            ~> inf_bool_eq
    1.70 +    join_bool_eq            ~> sup_bool_eq
    1.71 +    meet_fun_eq             ~> inf_fun_eq
    1.72 +    join_fun_eq             ~> sup_fun_eq
    1.73 +    meet_set_eq             ~> inf_set_eq
    1.74 +    join_set_eq             ~> sup_set_eq
    1.75 +    meet1_iff               ~> inf1_iff
    1.76 +    meet2_iff               ~> inf2_iff
    1.77 +    meet1I                  ~> inf1I
    1.78 +    meet2I                  ~> inf2I
    1.79 +    meet1D1                 ~> inf1D1
    1.80 +    meet2D1                 ~> inf2D1
    1.81 +    meet1D2                 ~> inf1D2
    1.82 +    meet2D2                 ~> inf2D2
    1.83 +    meet1E                  ~> inf1E
    1.84 +    meet2E                  ~> inf2E
    1.85 +    join1_iff               ~> sup1_iff
    1.86 +    join2_iff               ~> sup2_iff
    1.87 +    join1I1                 ~> sup1I1
    1.88 +    join2I1                 ~> sup2I1
    1.89 +    join1I1                 ~> sup1I1
    1.90 +    join2I2                 ~> sup1I2
    1.91 +    join1CI                 ~> sup1CI
    1.92 +    join2CI                 ~> sup2CI
    1.93 +    join1E                  ~> sup1E
    1.94 +    join2E                  ~> sup2E
    1.95 +
    1.96 +    is_meet_Meet            ~> is_meet_Inf
    1.97 +    Meet_bool_def           ~> Inf_bool_def
    1.98 +    Meet_fun_def            ~> Inf_fun_def
    1.99 +    Meet_greatest           ~> Inf_greatest
   1.100 +    Meet_lower              ~> Inf_lower
   1.101 +    Meet_set_def            ~> Inf_set_def
   1.102 +
   1.103 +    listsp_meetI            ~> listsp_infI
   1.104 +    listsp_meet_eq          ~> listsp_inf_eq
   1.105 +
   1.106  * Class (axclass + locale) "preorder" and "linear": facts "refl", "trans" and
   1.107  "cases" renamed ro "order_refl", "order_trans" and "linorder_cases", to
   1.108  avoid clashes with HOL "refl" and "trans". INCOMPATIBILITY.