# HG changeset patch
# User wenzelm
# Date 1684608973 -7200
# Node ID 90b64ffc48a35170a90913aab2d6d1afd5825321
# Parent  5edd5b12017d5c5c0c6791f98afc82cf98482a61
more documentation;

diff -r 5edd5b12017d -r 90b64ffc48a3 src/Doc/Implementation/Proof.thy
--- a/src/Doc/Implementation/Proof.thy	Sat May 20 17:42:01 2023 +0200
+++ b/src/Doc/Implementation/Proof.thy	Sat May 20 20:56:13 2023 +0200
@@ -271,6 +271,7 @@
   @{define_ML Assumption.add_assumes: "
   cterm list -> Proof.context -> thm list * Proof.context"} \\
   @{define_ML Assumption.export: "Proof.context -> Proof.context -> thm -> thm"} \\
+  @{define_ML Assumption.export_goal: "Proof.context -> Proof.context -> thm -> thm"} \\
   @{define_ML Assumption.export_term: "Proof.context -> Proof.context -> term -> term"} \\
   \end{mldecls}
 
@@ -292,9 +293,10 @@
 
   \<^descr> \<^ML>\<open>Assumption.export\<close>~\<open>inner outer thm\<close> exports result \<open>thm\<close> from the
   \<open>inner\<close> context back into the \<open>outer\<close> one; \<^ML>\<open>Assumption.export_goal\<close>
-  does the same in a goal context. The result is in HHF normal form. Note that
-  \<^ML>\<open>Proof_Context.export\<close> combines \<^ML>\<open>Variable.export\<close> and
-  \<^ML>\<open>Assumption.export\<close> in the canonical way.
+  does the same in a goal context (\<^theory_text>\<open>fix/assume/show\<close> in Isabelle/Isar). The
+  result is always in HHF normal form. Note that \<^ML>\<open>Proof_Context.export\<close>
+  combines \<^ML>\<open>Variable.export\<close> and \<^ML>\<open>Assumption.export\<close> in the
+  canonical way.
 
   \<^descr> \<^ML>\<open>Assumption.export_term\<close>~\<open>inner outer t\<close> exports term \<open>t\<close> from the
   \<open>inner\<close> context back into the \<open>outer\<close> one. This is analogous to