[isabelle-dev] Pow

[Robert Himmelmann]

There seem to be quite a few problems with find_theorems at the moment;
various searches do not return any results, e.g. prepending (100) to any
search. Changeset a03f3f9874f6 seems to be working whereas in
ada58d813783 the search is broken.

Robert Himmelmann

Tobias Nipkow schrieb:
> 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
>>     
>
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>