[isabelle] subst translated to ML-level ?



Hi all,

I cannot figure out how to write
 apply (subst theorem)
in the form:
 apply (tactic {* ... *})


The file Provers/eqsubst.thy seems to define this method, but it lacks documentation in the isabelle reference manual, the chapter on substitution there describes "stac" instead, which is not quite the same.

Maybe my question reduces to the stupid question: What to fill in for the parameters of "fun eqsubst_tac ctxt occL thms i th", when I want to use it inside an:
 apply (tactic {* ... *}) ?

Regards and thanks in advance for any help,
 Peter









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