Re: [isabelle] Giving a name to a tactics-expression
On Mon, 22 Feb 2010, Jeremy Dawson wrote:
Well, that is useful information of a negative nature. It tells me how you
_don't_ do the following:
val meth4 = EVERY [(TRY (REPEAT1 meth1)), meth2, meth3 ] ;
But the question is how _do_ you do it.
You don't, but go down to the basic tactics behind meth1, meth2, meth3.
(All tools are supposed to export this ML view, apart from defining
end-user method syntax.)
Isar methods are a more stylized way of refining structured goals than
tactics, and things like fine-grained goal addressing is missing. This
makes user space method expressions more digestible than old tactical ones
-- you certainly know how proof scripts looked 10 years ago -- but on the
other hand it is harder to define meaningful method combinations.
So just compose things as a tactic and then link it up with Isar via
method_setup. There are plenty of examples in the sources -- most of them
quite clean, because I've reworked these interfaces for Isabelle2009.
This archive was generated by a fusion of
Pipermail (Mailman edition) and