Re: [isabelle] insert for one subgoal?



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.

The reason is to make things work most of the time, without the explicit goal addressing of the pre-Isar tactical proof style.

This question shows up only every 5 years or so, which means Isar was successful here.


	Makarius





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