[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?

Thanks,
GB






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