[isabelle] Are unnamed theorems used by automatic methods or Sledgehammer?

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?


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