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
Last updated: Dec 07 2023 at 16:21 UTC