[isabelle] subst_tac?

The subst method is great, I use it a lot (thanks Lucas!). Is there a _tac version of subst that would allow me to instantiate the rewrite rule supplied with expressions that contain meta-bound variables of the subgoal?


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