Re: [isabelle] insert for one subgoal?
wow, this is uber-useful. especially apply auto 
thank you, Peter.
this is not in the tutorial, isn't it? i think it should.
(i found only the direct subgoal addressing with [n] of *_tac)
2012/4/11 Peter Lammich <lammich at in.tum.de>
> 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
> No idea what the reason is why some commands (auto, insert, etc) work on
> all goals, while others (blast, force, etc. ) do not.
> On Mi, 2012-04-11 at 16:53 +0200, Nils Jähnig wrote:
> > Hello,
> > when I use apply(insert thm), thm gets inserted into all subgoals.
> > cluttering up premises is usually unwanted.
> > now i use subgoal_tac and prove the resulting new subgoal to achieve
> > getting a thm inserted in just one subgoal, but maybe there is an easier
> > way, something like insert1?
> > what is the reason for insert inserting into all subgoals?
> > Best Regards
> > Nils
This archive was generated by a fusion of
Pipermail (Mailman edition) and