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

[Lawrence Paulson]

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.

Larry

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>