[isabelle] Method combinator ; restricts to first subgoal
I am wondering why the new method combinator restricts the first method to the first
subgoal. Is there any deeper reason for this design decision?
I regularly attempt myself to write things like the following
apply(auto; force intro: ...)
apply(case_tac [1-3] x; simp_all)
and then wonder why they don't work as expected (throw the first method at all/the
specified subgoals and then invoke the second method only on subgoals arising from the
first method). What are the use cases for the restriction to the first subgoal? Or am I
just using bad style?
This archive was generated by a fusion of
Pipermail (Mailman edition) and