equal
deleted
inserted
replaced
12 subsection \<open>Export and re-import of global proof terms\<close> |
12 subsection \<open>Export and re-import of global proof terms\<close> |
13 |
13 |
14 ML \<open> |
14 ML \<open> |
15 fun export_proof thy thm = |
15 fun export_proof thy thm = |
16 Proofterm.encode (Sign.consts_of thy) |
16 Proofterm.encode (Sign.consts_of thy) |
17 (Proofterm.reconstruct_proof thy (Thm.prop_of thm) (Thm.standard_proof_of true thm)); |
17 (Proofterm.reconstruct_proof thy (Thm.prop_of thm) |
|
18 (Thm.standard_proof_of {full = true, expand = [Thm.raw_derivation_name thm]} thm)); |
18 |
19 |
19 fun import_proof thy xml = |
20 fun import_proof thy xml = |
20 let |
21 let |
21 val prf = Proofterm.decode (Sign.consts_of thy) xml; |
22 val prf = Proofterm.decode (Sign.consts_of thy) xml; |
22 val (prf', _) = Proofterm.freeze_thaw_prf prf; |
23 val (prf', _) = Proofterm.freeze_thaw_prf prf; |