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 a syntax 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, ML function `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) ?

TL; DR: How do I use a ML function returning a value of type `thm`

to prove a theorem in the outer syntax ?

See page 18 of the ML cookbook. In particular, you are looking for the function `Local_Theory.note`

.

Last updated: Dec 07 2023 at 16:21 UTC