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: Nov 11 2024 at 04:22 UTC