[isabelle] insert for one subgoal?


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

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