From: Yann Leray <yann.leray@inria.fr>

Hi,

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

Yann Leray

Last updated: Sep 25 2021 at 09:17 UTC