Stream: Isabelle/ML

Topic: Interface between Isabelle/ML and regular Isabelle

view this post on Zulip Yann Leray (Jul 09 2021 at 19:12):

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 ?

view this post on Zulip Lukas Stevens (Jul 09 2021 at 19:24):

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