equal
deleted
inserted
replaced
10 begin |
10 begin |
11 |
11 |
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 = thm |
16 Proofterm.encode (Sign.consts_of thy) |
16 |> Thm.standard_proof_of {full = true, expand_name = Thm.expand_name thm} |
17 (Proofterm.reconstruct_proof thy (Thm.prop_of thm) |
17 |> Proofterm.encode (Sign.consts_of thy); |
18 (Thm.standard_proof_of {full = true, expand_name = Thm.expand_name thm} thm)); |
|
19 |
18 |
20 fun import_proof thy xml = |
19 fun import_proof thy xml = |
21 let |
20 let |
22 val prf = Proofterm.decode (Sign.consts_of thy) xml; |
21 val prf = Proofterm.decode (Sign.consts_of thy) xml; |
23 val (prf', _) = Proofterm.freeze_thaw_prf prf; |
22 val (prf', _) = Proofterm.freeze_thaw_prf prf; |