[isabelle-dev] NEWS

[Florian Haftmann]

Changes culminated over the last 12 months:

Refinements to lattice classes and sets:
  - less default intro/elim rules in locale variant, more default
    intro/elim rules in class variant: more uniformity
  - lemma ge_sup_conv renamed to le_sup_iff, in accordance with
    le_inf_iff
  - dropped lemma alias inf_ACI for inf_aci (same for sup_ACI and
    sup_aci)
  - renamed ACI to inf_sup_aci
  - new class "boolean_algebra"
  - class "complete_lattice" moved to separate theory
    "complete_lattice";
    corresponding constants (and abbreviations) renamed and with
    authentic syntax:
    Set.Inf ~>      Complete_Lattice.Inf
    Set.Sup ~>      Complete_Lattice.Sup
    Set.INFI ~>     Complete_Lattice.INFI
    Set.SUPR ~>     Complete_Lattice.SUPR
    Set.Inter ~>    Complete_Lattice.Inter
    Set.Union ~>    Complete_Lattice.Union
    Set.INTER ~>    Complete_Lattice.INTER
    Set.UNION ~>    Complete_Lattice.UNION
  - more convenient names for set intersection and union:
    Set.Int ~>      Set.inter
    Set.Un ~>       Set.union
  - authentic syntax for
    Set.Pow
    Set.image
  - mere abbreviations:
    Set.empty               (for bot)
    Set.UNIV                (for top)
    Set.inter               (for inf)
    Set.union               (for sup)
    Complete_Lattice.Inter  (for Inf)
    Complete_Lattice.Union  (for Sup)
    Complete_Lattice.INTER  (for INFI)
    Complete_Lattice.UNION  (for SUPR)
  - object-logic definitions as far as appropriate

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 260 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20090925/77213c60/attachment.sig>