# HG changeset patch
# User wenzelm
# Date 1455890498 -3600
# Node ID 7b5468422352fd106a4d305c7aec73d3e90bea5c
# Parent  e4119d366ab001c6ac7711e0672ac13024ac0a8a
moved examples to avoid dependency on bulky HOL-Proofs session, e.g. relevant for "isabelle makedist";

diff -r e4119d366ab0 -r 7b5468422352 src/Doc/Implementation/Logic.thy
--- 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
diff -r e4119d366ab0 -r 7b5468422352 src/Doc/ROOT
--- a/src/Doc/ROOT	Fri Feb 19 14:50:12 2016 +0100
+++ b/src/Doc/ROOT	Fri Feb 19 15:01:38 2016 +0100
@@ -125,7 +125,7 @@
     "getting.tex"
     "root.tex"
 
-session Implementation (doc) in "Implementation" = "HOL-Proofs" +
+session Implementation (doc) in "Implementation" = "HOL" +
   options [document_variants = "implementation", quick_and_dirty]
   theories
     Eq
diff -r e4119d366ab0 -r 7b5468422352 src/HOL/Proofs/ex/Proof_Terms.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Proofs/ex/Proof_Terms.thy	Fri Feb 19 15:01:38 2016 +0100
@@ -0,0 +1,62 @@
+(*  Title:      HOL/Proofs/ex/Proof_Terms.thy
+    Author:     Makarius
+
+Basic examples involving proof terms.
+*)
+
+theory Proof_Terms
+imports Main
+begin
+
+text \<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>
+
+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>
+
+end
diff -r e4119d366ab0 -r 7b5468422352 src/HOL/ROOT
--- a/src/HOL/ROOT	Fri Feb 19 14:50:12 2016 +0100
+++ b/src/HOL/ROOT	Fri Feb 19 15:01:38 2016 +0100
@@ -402,6 +402,7 @@
   options [document = false, parallel_proofs = 0]
   theories
     Hilbert_Classical
+    Proof_Terms
     XML_Data
 
 session "HOL-Proofs-Extraction" in "Proofs/Extraction" = "HOL-Proofs" +