[isabelle] How to retrieve theorems defined in ML
- To: cl-isabelle-users at lists.cam.ac.uk
- Subject: [isabelle] How to retrieve theorems defined in ML
- From: Yann Leray <yann.leray at inria.fr>
- Date: Thu, 8 Jul 2021 15:34:59 +0200
- Authentication-results: cam.ac.uk; iprev=pass (mail2-relais-roc.national.inria.fr) smtp.remote-ip=126.96.36.199; spf=pass smtp.mailfrom=inria.fr; arc=none
- Ironport-hdrordr: A9a23:rp5o1KOgddWHocBcThijsMiBIKoaSvp037BL7SxMoHluGfBw+PrAoB1l73HJYVoqOU3Is+rhBED4ewK+yXct2/hyAV7AZniChILXFvAH0WK4+UyGJ8SWzIc06U4HSdkZNDSaNzVHZKjBijVR57wbsaC6GdiT9J/jJ/wHd3AQV0nrhD0JcDpyqyZNNXR7OaY=
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:78.0) Gecko/20100101 Thunderbird/78.11.0
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and