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>

> Hi,
>
> 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.
>
> Best
>   Peter
>
> 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 MHonArc.