*To*: Peter Lammich <lammich at in.tum.de>*Subject*: Re: [isabelle] insert for one subgoal?*From*: Makarius <makarius at sketis.net>*Date*: Wed, 11 Apr 2012 20:11:25 +0200 (CEST)*Cc*: isabelle-users at cl.cam.ac.uk, Nils Jähnig <jaehnig at mi.fu-berlin.de>*In-reply-to*: <1334158106.19699.99.camel@lapbroy33>*References*: <CACU92SASVJY055ESrXtVLf90spO1pfZG-Aj9Qo4FKKqePzvETQ@mail.gmail.com> <1334158106.19699.99.camel@lapbroy33>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Wed, 11 Apr 2012, Peter Lammich wrote:

try "apply (insert xxx) []". The []-Syntax restricts the effect of any apply-command to the first subgoal. There is also [n] to restrict the effect to the first n subgoals. No idea what the reason is why some commands (auto, insert, etc) work on all goals, while others (blast, force, etc. ) do not.

Makarius

**References**:**[isabelle] insert for one subgoal?***From:*Nils Jähnig

**Re: [isabelle] insert for one subgoal?***From:*Peter Lammich

- Previous by Date: Re: [isabelle] insert for one subgoal?
- Next by Date: Re: [isabelle] insert for one subgoal?
- Previous by Thread: Re: [isabelle] insert for one subgoal?
- Next by Thread: [isabelle] Parametric theories
- Cl-isabelle-users April 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list