Re: [isabelle] any way to increase force search depth?
Andrei Borac wrote:
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
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?
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
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