[isabelle] How to retrieve theorems defined in ML



Hi,

I'd like to use the proof term syntax, as defined in implementation §2.5, to prove theorems (more precisely, I'd like to translate some proof terms to asyntax understood by Isabelle).

However, there is no mention in this documentation of a command to use the proof term to prove theorems directly inside Isabelle.

As far as I understand, `Proof_Checker.thm_of_proof` can return a value of the type thm, which is what I would want, but I don't know how to export it as a theorem in Isabelle.


How should I do to export this returned value (if I understood well) ?

Thanks for your time
Yann Leray




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