[isabelle-dev] NEWS: Revision of Big Operators on sets

[Florian Haftmann]

* Revised devices for recursive definitions over finite sets:
  - Only one fundamental fold combinator on finite set remains:
    Finite_Set.fold :: ('a => 'b => 'b) => 'b => 'a set => 'b
    This is now identity on infinite sets.
  - Locales (»mini packages«) for fundamental definitions with
    Finite_Set.fold: folding, folding_idem.
  - Locales comm_monoid_set, semilattice_order_set and
    semilattice_neutr_order_set for big operators on sets.
    See theory Big_Operators for canonical examples.
    Note that foundational constants comm_monoid_set.F and
    semilattice_set.F correspond to former combinators fold_image
    and fold1 respectively.  These are now gone.  You may use
    those foundational constants as substitutes, but it is
    preferable to interpret the above locales accordingly.
  - Dropped class ab_semigroup_idem_mult (special case of lattice,
    no longer needed in connection with Finite_Set.fold etc.)
  - Fact renames:
      card.union_inter ~> card_Un_Int [symmetric]
      card.union_disjoint ~> card_Un_disjoint

INCOMPATIBILITY.

This refers to 7edcc0618dae.

	Florian

-- 

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: 261 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20130323/cd1485d7/attachment.asc>