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
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and