Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] How to retrieve theorems defined in ML


view this post on Zulip Email Gateway (Jul 08 2021 at 13:35):

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