Re: [isabelle] Quick question about rule+

On Thu, 3 Sep 2009, Peter Lammich wrote:

()+ is a tactic that repeats its argument tactic until it fails, at least once.

Note that a "tactic" is just a low-level refinement operation on a goal state. In Isabelle type tactic = thm -> thm Seq.seq, i.e. lazy map from state to any number of possible successor states. (Each state is of the form subgoals ==> main_goal.)

A "tactical" is a higher-order tactic combinator, such as THEN, REPEAT, etc.

In Isar, a "method" is a bit like a "rich tactic", with extra information about context and used facts, and with potential results of "cases" (as in the "induct" method).

So the "+" operator above would be a "methodical", but this terminology is not used.


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