[isabelle] Program extraction, accessing instantiated proof terms



Hello,

I am trying to understand the implementation of program extraction in Isabelle. I am wondering whether it is possible to access the instantiated proof terms (like the output of the Isar commands prf or full_prf) in the extract/extr functions in Pure/Proof/extraction.ml.

I tried printing them for better understanding and thought it should be possible similar as in string_of_prfs (in Pure/Isar/isar_cmd.ML), but I don't know how to access the context, or if it is even possible at this point.

Is there an easy way to access the instantiated proof terms in the extr functions?

Thank you and best regards,
Matthias




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.