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> 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) [1]

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 MHonArc.