| changeset 70830 | 8f050cc0ec50 |
| parent 70449 | 6e34025981be |
| child 70839 | 2136e4670ad2 |
| 70829:1fa55b0873bc | 70830:8f050cc0ec50 |
|---|---|
21 |
21 |
22 ML_val \<open> |
22 ML_val \<open> |
23 val thm = @{thm ex}; |
23 val thm = @{thm ex}; |
24 |
24 |
25 (*proof body with digest*) |
25 (*proof body with digest*) |
26 val body = Proofterm.strip_thm (Thm.proof_body_of thm); |
26 val body = Proofterm.strip_thm_body (Thm.proof_body_of thm); |
27 |
27 |
28 (*proof term only*) |
28 (*proof term only*) |
29 val prf = Proofterm.proof_of body; |
29 val prf = Proofterm.proof_of body; |
30 |
30 |
31 (*clean output*) |
31 (*clean output*) |