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.


	Makarius





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