[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?

Thanks,
-john






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