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.

Larry Paulson


> 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
> sledgehammer. 





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.