[isabelle] Method combinator ; restricts to first subgoal

Dear all,

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(safe; simp_all)
  apply(simp_all; blast)
  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 MHonArc.