Re: [isabelle] Difference between "apply(auto)" and "apply(force)"



On Wed, May 2, 2012 at 1:04 AM, Ridgway, John V. E. <
John.Ridgway at trincoll.edu> wrote:

> Furthermore, at another place in the proof, when I try apply(auto) it ends
> me up with a goal of False, whereas when I try apply(force)+ I don't have
> the patience to wait for it to finish..


That might mean your goal is unprovable (and you should double-check your
theorem statement...).
(It could also mean that there are contradictions in your assumptions or
context somewhere that auto hasn't noticed.)
I guess apply(force) in that place is "never giving up" (as Larry said)
trying to prove an unprovable goal, and therefore running forever.




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