[isabelle-dev] Pow

Tobias Nipkow nipkow at in.tum.de
Mon Dec 14 13:46:49 CET 2009


I get to see 21 thms. Are you sure Set is included as an ancestor, eg
via Main?

Tobias

Lawrence Paulson wrote:
> Anybody know why "find theorems" can find nothing about the power set operator? Other set theoretic primitives, such as Union and insert, work fine.
> Larry
> 
> 
> ------------------------------------------------------------------------
> 
> 
> ------------------------------------------------------------------------
> 
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev




More information about the isabelle-dev mailing list