[isabelle] resolve current subgoal with matching premise
is there an easy way in Isabelle/ML to replace the current subgoal by
the assumptions of the first premise whose conclusion matches it?
I have a subgoal of the shape
!! a1 ... aN.
(!! b1 ... bK. ...) ==>
(!! i1 ... iM. ... ==> P iI) (*[*]*) ==>
(!! z1 ... zL. ...) ==> P aJ
and would like to replace it by the premises of [*]. I think this should
be easy but could figure it out immediately.
The reason why I'm asking is that "blast_tac" is very slow on some goals
of this shape that I obtain by another hand-written tactic and I hope to
speed things up.
This archive was generated by a fusion of
Pipermail (Mailman edition) and