[isabelle-dev] Some proposed extensions to the Isabelle library

Lawrence Paulson lp15 at cam.ac.uk
Sat Sep 21 10:12:07 CEST 2013

Some of the results in subsection {* Sets *} may be interesting. But your product distribution laws are subsumed by the Sigma_XX_distrib{1,2} laws in Product_Type.thy.

As for indexed products, check the existing HOL/Library/FuncSet.thy for possible overlaps.


On 21 Sep 2013, at 03:08, Alessandro Coglio <coglio at kestrel.edu> wrote:

> A theory of indexed products, modeled via maps and also modeled via functions.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20130921/09f9968b/attachment-0002.html>

More information about the isabelle-dev mailing list