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://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20090925/77213c60/attachment.pgp>
