Re: [isabelle] insert for one subgoal?



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.