Re: [isabelle] question about locales and locale parameters
On Mon, 19 Apr 2010, Brian Huffman wrote:
On Mon, Apr 19, 2010 at 10:48 AM, Viorel Preoteasa
<viorel.preoteasa at abo.fi> wrote:
Is there a way of applying a rule (auto, safe, clarify, unfold) only
to the first goal (the same way as simp works)?
Yes, try the following:
apply (auto) 
In general, "apply (<tactic>) [n]" restricts the tactic to act only on
the first n subgoals.
Here I really need to insist that the Isar category of "method" is not
called "tactic". One of the very characteristics of Isar proof methods is
the stylized access to the underlying goal structure, without the
traditional goal addressing of tactics.
The method combinator [...] above works quite differently from tactial
goal addressing: it singles out a section of the goal state, applies the
proof method, and retrofits the result.
This archive was generated by a fusion of
Pipermail (Mailman edition) and