--- a/src/Doc/Implementation/Logic.thy Fri Feb 19 14:50:12 2016 +0100
+++ b/src/Doc/Implementation/Logic.thy Fri Feb 19 15:01:38 2016 +0100
@@ -1248,60 +1248,11 @@
\<close>
text %mlex \<open>
- Detailed proof information of a theorem may be retrieved as follows:
-\<close>
-
-lemma ex: "A \<and> B \<longrightarrow> B \<and> A"
-proof
- assume "A \<and> B"
- then obtain B and A ..
- then show "B \<and> A" ..
-qed
-
-ML_val \<open>
- (*proof body with digest*)
- val body = Proofterm.strip_thm (Thm.proof_body_of @{thm ex});
-
- (*proof term only*)
- val prf = Proofterm.proof_of body;
- Pretty.writeln (Proof_Syntax.pretty_proof @{context} prf);
-
- (*all theorems used in the graph of nested proofs*)
- val all_thms =
- Proofterm.fold_body_thms
- (fn (name, _, _) => insert (op =) name) [body] [];
-\<close>
+ \<^item> @{file "~~/src/HOL/Proofs/ex/Proof_Terms.thy"} provides basic examples
+ involving proof terms.
-text \<open>
- The result refers to various basic facts of Isabelle/HOL: @{thm [source]
- HOL.impI}, @{thm [source] HOL.conjE}, @{thm [source] HOL.conjI} etc. The
- combinator @{ML Proofterm.fold_body_thms} recursively explores the graph of
- the proofs of all theorems being used here.
-
- \<^medskip>
- Alternatively, we may produce a proof term manually, and turn it into a
- theorem as follows:
-\<close>
-
-ML_val \<open>
- val thy = @{theory};
- val prf =
- Proof_Syntax.read_proof thy true false
- "impI \<cdot> _ \<cdot> _ \<bullet> \
- \ (\<^bold>\<lambda>H: _. \
- \ conjE \<cdot> _ \<cdot> _ \<cdot> _ \<bullet> H \<bullet> \
- \ (\<^bold>\<lambda>(H: _) Ha: _. conjI \<cdot> _ \<cdot> _ \<bullet> Ha \<bullet> H))";
- val thm =
- prf
- |> Reconstruct.reconstruct_proof thy @{prop "A \<and> B \<longrightarrow> B \<and> A"}
- |> Proof_Checker.thm_of_proof thy
- |> Drule.export_without_context;
-\<close>
-
-text \<open>
- \<^medskip>
- See also @{file "~~/src/HOL/Proofs/ex/XML_Data.thy"} for further examples,
- with export and import of proof terms via XML/ML data representation.
+ \<^item> @{file "~~/src/HOL/Proofs/ex/XML_Data.thy"} demonstrates export and import
+ of proof terms via XML/ML data representation.
\<close>
end