Re: [isabelle] question about locales and locale parameters



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

In general, "apply (<tactic>) [n]" restricts the tactic to act only on
the first n subgoals.

- Brian





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