equal
deleted
inserted
replaced
28 Pretty.writeln (Proof_Syntax.pretty_proof @{context} prf); |
28 Pretty.writeln (Proof_Syntax.pretty_proof @{context} prf); |
29 |
29 |
30 (*all theorems used in the graph of nested proofs*) |
30 (*all theorems used in the graph of nested proofs*) |
31 val all_thms = |
31 val all_thms = |
32 Proofterm.fold_body_thms |
32 Proofterm.fold_body_thms |
33 (fn (name, _, _) => insert (op =) name) [body] []; |
33 (fn {name, ...} => insert (op =) name) [body] []; |
34 \<close> |
34 \<close> |
35 |
35 |
36 text \<open> |
36 text \<open> |
37 The result refers to various basic facts of Isabelle/HOL: @{thm [source] |
37 The result refers to various basic facts of Isabelle/HOL: @{thm [source] |
38 HOL.impI}, @{thm [source] HOL.conjE}, @{thm [source] HOL.conjI} etc. The |
38 HOL.impI}, @{thm [source] HOL.conjE}, @{thm [source] HOL.conjI} etc. The |