equal
deleted
inserted
replaced
12 subsection {* Export and re-import of global proof terms *} |
12 subsection {* Export and re-import of global proof terms *} |
13 |
13 |
14 ML {* |
14 ML {* |
15 fun export_proof thy thm = |
15 fun export_proof thy thm = |
16 let |
16 let |
17 val {prop, hyps, shyps, ...} = Thm.rep_thm thm; |
17 val (_, prop) = |
18 val (_, prop) = Logic.unconstrainT shyps (Logic.list_implies (hyps, prop)); |
18 Logic.unconstrainT (Thm.shyps_of thm) |
|
19 (Logic.list_implies (Thm.hyps_of thm, Thm.prop_of thm)); |
19 val prf = |
20 val prf = |
20 Proofterm.proof_of (Proofterm.strip_thm (Thm.proof_body_of thm)) |> |
21 Proofterm.proof_of (Proofterm.strip_thm (Thm.proof_body_of thm)) |> |
21 Reconstruct.reconstruct_proof thy prop |> |
22 Reconstruct.reconstruct_proof thy prop |> |
22 Reconstruct.expand_proof thy [("", NONE)] |> |
23 Reconstruct.expand_proof thy [("", NONE)] |> |
23 Proofterm.rew_proof thy |> |
24 Proofterm.rew_proof thy |> |