Re: [isabelle] find_theorems and locales
I agree with this view. There are many theorems that probably shouldnât be given to sledgehammer, though the only justification for this would be that they are unlikely to be helpful for finding proofs. But it should be possible to search for them. I have been tripped up here as well.
> On 12 Jun 2015, at 08:40, Bertram Felgenhauer <bertram.felgenhauer at googlemail.com> wrote:
> Secondly, I feel that there is a tangible advantage of making these
> facts available, which to my mind means that they should also be
> discoverable through find_theorems, though not necessarily by
This archive was generated by a fusion of
Pipermail (Mailman edition) and