--- a/src/Doc/Implementation/Proof.thy Fri Jan 21 23:49:10 2022 +0000
+++ b/src/Doc/Implementation/Proof.thy Sat Jan 22 13:00:03 2022 +0100
@@ -271,11 +271,12 @@
@{define_ML Assumption.add_assumes: "
cterm list -> Proof.context -> thm list * Proof.context"} \\
@{define_ML Assumption.export: "bool -> Proof.context -> Proof.context -> thm -> thm"} \\
+ @{define_ML Assumption.export_term: "Proof.context -> Proof.context -> term -> term"} \\
\end{mldecls}
- \<^descr> Type \<^ML_type>\<open>Assumption.export\<close> represents arbitrary export rules, which
- is any function of type \<^ML_type>\<open>bool -> cterm list -> thm -> thm\<close>, where
- the \<^ML_type>\<open>bool\<close> indicates goal mode, and the \<^ML_type>\<open>cterm list\<close>
+ \<^descr> Type \<^ML_type>\<open>Assumption.export\<close> represents export rules, as a pair of
+ functions \<^ML_type>\<open>bool -> cterm list -> (thm -> thm) * (term -> term)\<close>.
+ The \<^ML_type>\<open>bool\<close> argument indicates goal mode, and the \<^ML_type>\<open>cterm list\<close>
the collection of assumptions to be discharged simultaneously.
\<^descr> \<^ML>\<open>Assumption.assume\<close>~\<open>ctxt A\<close> turns proposition \<open>A\<close> into a primitive
@@ -285,13 +286,21 @@
with export rule \<open>r\<close>. The resulting facts are hypothetical theorems as
produced by the raw \<^ML>\<open>Assumption.assume\<close>.
- \<^descr> \<^ML>\<open>Assumption.add_assumes\<close>~\<open>As\<close> is a special case of \<^ML>\<open>Assumption.add_assms\<close> where the export rule performs \<open>\<Longrightarrow>\<hyphen>intro\<close> or
+ \<^descr> \<^ML>\<open>Assumption.add_assumes\<close>~\<open>As\<close> is a special case of
+ \<^ML>\<open>Assumption.add_assms\<close> where the export rule performs \<open>\<Longrightarrow>\<hyphen>intro\<close> or
\<open>#\<Longrightarrow>\<hyphen>intro\<close>, depending on goal mode.
\<^descr> \<^ML>\<open>Assumption.export\<close>~\<open>is_goal inner outer thm\<close> exports result \<open>thm\<close>
- from the the \<open>inner\<close> context back into the \<open>outer\<close> one; \<open>is_goal = true\<close>
- means this is 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.
+ from the \<open>inner\<close> context back into the \<open>outer\<close> one; \<open>is_goal = true\<close> means
+ this is 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.
+
+ \<^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
+ \<^ML>\<open>Assumption.export\<close>, but only takes syntactical aspects of the
+ context into account (such as locally specified variables as seen in
+ @{command define} or @{command obtain}).
\<close>
text %mlex \<open>