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 <cog...@kestrel.edu> wrote:
> A theory of indexed products, modeled via maps and also modeled via functions.
>
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
