[isabelle-dev] Products over lists – naming convention for big sums and products.

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Thu Sep 18 15:47:06 CEST 2014

Changeset #fe083c681ed8 introduces products over lists.  There has been
some private discussion whether there could be a serious attempt to
establish a new consistent naming scheme for summation and products over

a) for lists: sum_list (← listsum), prod_list (← listprod)
b) for multisets: Sum_mset (← msetsum), Prod_mset (← msetprod)
c) for finite sets: Sum (← setsum), Prod (← setprod)
As far as can be forseen, 58 theories would be affected by a switch as
suggested by a). b) is no big issue. c) is maybe beyond what should be
reasonably attempted (218 affected theories).
Suggestions welcome.


PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 181 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20140918/37ad76e7/attachment.asc>

More information about the isabelle-dev mailing list