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

Tobias Nipkow nipkow at in.tum.de
Thu Sep 18 16:11:10 CEST 2014

On 18/09/2014 15:47, Florian Haftmann wrote:
> 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 
> collections.
> 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)

Looking again at the result of our discussion I still like it.


> 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.  
> Cheers, Florian
> _______________________________________________ isabelle-dev mailing list 
> isabelle-dev at in.tum.de 
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

More information about the isabelle-dev mailing list