Re: [isabelle] any way to increase force search depth?

Andrei Borac wrote:
Or perhaps someone can give me few pointers to places in Isabelle's
source or code samples that are relevant to writing such a trial and
error tactic in ML?

It all rather depends on the nature of your problem, but I find that you can often pick out the easy subgoals in a way which will give you the right instantiations.

Things like this

(TRYALL (ares_tac [refl])), (TRYALL (eresolve_tac wf_cc_Ds)),

tend to be sprinkled throughout my proofs, and I don't have to do much instantiating by "hand", or, for that matter, waiting for Force_tac to finish.

So far as I know these tactics have no equivalent in Isar. Opinions seem to vary as to whether that is a reason for not using them



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