Re: [isabelle] Are unnamed theorems used by automatic methods or Sledgehammer?
On Fri, 24 Aug 2012, Gottfried Barrow wrote:
Suppose I have an unnamed theorem:
theorem "<some formula that's true>" by(auto)
Are automatic proof methods, or is Sledgehammer going to try and use that
theorem to prove anything?
When it is really unnamed and has not other attributes to declare it to
the context, the system will not store the theorem anywhere. So other
tools like sledgehammer should not be able to find it.
This archive was generated by a fusion of
Pipermail (Mailman edition) and