equal
deleted
inserted
replaced
18 then obtain B and A .. |
18 then obtain B and A .. |
19 then show "B \<and> A" .. |
19 then show "B \<and> A" .. |
20 qed |
20 qed |
21 |
21 |
22 ML_val \<open> |
22 ML_val \<open> |
|
23 val thm = @{thm ex}; |
|
24 |
23 (*proof body with digest*) |
25 (*proof body with digest*) |
24 val body = Proofterm.strip_thm (Thm.proof_body_of @{thm ex}); |
26 val body = Proofterm.strip_thm (Thm.proof_body_of thm); |
25 |
27 |
26 (*proof term only*) |
28 (*proof term only*) |
27 val prf = Proofterm.proof_of body; |
29 val prf = Proofterm.proof_of body; |
28 Pretty.writeln (Proof_Syntax.pretty_proof @{context} prf); |
30 |
|
31 (*clean output*) |
|
32 Pretty.writeln (Proof_Syntax.pretty_clean_proof_of @{context} false thm); |
|
33 Pretty.writeln (Proof_Syntax.pretty_clean_proof_of @{context} true thm); |
29 |
34 |
30 (*all theorems used in the graph of nested proofs*) |
35 (*all theorems used in the graph of nested proofs*) |
31 val all_thms = |
36 val all_thms = |
32 Proofterm.fold_body_thms |
37 Proofterm.fold_body_thms |
33 (fn {name, ...} => insert (op =) name) [body] []; |
38 (fn {name, ...} => insert (op =) name) [body] []; |