
diff -r ab1d60e1ee31 -r 73c1ad6eda9d doc-src/IsarImplementation/Thy/document/proof.tex
--- a/doc-src/IsarImplementation/Thy/document/proof.tex	Fri Sep 01 20:17:31 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/proof.tex	Fri Sep 01 20:40:05 2006 +0200
@@ -42,7 +42,8 @@
 \begin{mldecls}
   \indexml{Variable.declare-term}\verb|Variable.declare_term: term -> Proof.context -> Proof.context| \\
   \indexml{Variable.add-fixes}\verb|Variable.add_fixes: string list -> Proof.context -> string list * Proof.context| \\
-  \indexml{Variable.import}\verb|Variable.import: bool -> thm list -> Proof.context -> ((ctyp list * cterm list) * thm list) * Proof.context| \\
+  \indexml{Variable.import}\verb|Variable.import: bool ->|\isasep\isanewline%
+\verb|  thm list -> Proof.context -> ((ctyp list * cterm list) * thm list) * Proof.context| \\
   \indexml{Variable.export}\verb|Variable.export: Proof.context -> Proof.context -> thm list -> thm list| \\
   \indexml{Variable.trade}\verb|Variable.trade: Proof.context -> (thm list -> thm list) -> thm list -> thm list| \\
   \indexml{Variable.polymorphic}\verb|Variable.polymorphic: Proof.context -> term list -> term list| \\
@@ -119,17 +120,17 @@
   and more explicit references to hypotheses: \isa{A\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ A\isactrlisub n\ {\isasymturnstile}\ B} where \isa{A\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ A\isactrlisub n} needs to
   be covered by the assumptions of the current context.
 
-  \medskip The \isa{add{\isacharunderscore}assm} operation augments the context by
-  local assumptions, parameterized by an \isa{export} rule (see
-  below).
+  \medskip The \isa{add{\isacharunderscore}assms} operation augments the context by
+  local assumptions, which are parameterized by an arbitrary \isa{export} rule (see below).
 
   The \isa{export} operation moves facts from a (larger) inner
   context into a (smaller) outer context, by discharging the
   difference of the assumptions as specified by the associated export
   rules.  Note that the discharged portion is determined by the
-  contexts, not the facts being exported!  There is a separate flag to
-  indicate a goal context, where the result is meant to refine an
-  enclosing sub-goal of a structured proof state (cf.\ FIXME).
+  difference contexts, not the facts being exported!  There is a
+  separate flag to indicate a goal context, where the result is meant
+  to refine an enclosing sub-goal of a structured proof state (cf.\
+  \secref{sec:isar-proof-state}).
 
   \medskip The most basic export rule discharges assumptions directly
   by means of the \isa{{\isasymLongrightarrow}} introduction rule:
@@ -144,13 +145,11 @@
   \infer[(\isa{{\isacharhash}{\isasymLongrightarrow}{\isacharunderscore}intro})]{\isa{{\isasymGamma}\ {\isacharbackslash}\ A\ {\isasymturnstile}\ {\isacharhash}A\ {\isasymLongrightarrow}\ B}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B}}
   \]
 
-  \medskip Alternative versions of assumptions may perform arbitrary
-  transformations as long as a particular portion of hypotheses is
-  removed from the given facts.
-
-  For example, a local definition works by fixing \isa{x} and
-  assuming \isa{x\ {\isasymequiv}\ t}, with the following export rule to reverse
-  the effect:
+  \medskip Alternative assumptions may perform arbitrary
+  transformations on export, as long as a particular portion of
+  hypotheses is removed from the given facts.  For example, a local
+  definition works by fixing \isa{x} and assuming \isa{x\ {\isasymequiv}\ t},
+  with the following export rule to reverse the effect:
   \[
   \infer{\isa{{\isasymGamma}\ {\isacharbackslash}\ x\ {\isasymequiv}\ t\ {\isasymturnstile}\ B\ t}}{\isa{{\isasymGamma}\ {\isasymturnstile}\ B\ x}}
   \]
@@ -161,9 +160,9 @@
 
   \medskip
   \begin{tabular}{l}
-  \isa{add{\isacharunderscore}assm\ e\isactrlisub {\isadigit{1}}\ A\isactrlisub {\isadigit{1}}} \\
+  \isa{add{\isacharunderscore}assms\ e\isactrlisub {\isadigit{1}}\ A\isactrlisub {\isadigit{1}}} \\
   \isa{{\isasymdots}} \\
-  \isa{add{\isacharunderscore}assm\ e\isactrlisub n\ A\isactrlisub n} \\
+  \isa{add{\isacharunderscore}assms\ e\isactrlisub n\ A\isactrlisub n} \\
   \isa{export} \\
   \end{tabular}
   \medskip
@@ -184,31 +183,36 @@
 \begin{mldecls}
   \indexmltype{Assumption.export}\verb|type Assumption.export| \\
   \indexml{Assumption.assume}\verb|Assumption.assume: cterm -> thm| \\
-  \indexml{Assumption.add-assumes}\verb|Assumption.add_assumes: cterm list -> Proof.context -> thm list * Proof.context| \\
-  \indexml{Assumption.add-assms}\verb|Assumption.add_assms: Assumption.export -> cterm list -> Proof.context -> thm list * Proof.context| \\
+  \indexml{Assumption.add-assms}\verb|Assumption.add_assms: Assumption.export ->|\isasep\isanewline%
+\verb|  cterm list -> Proof.context -> thm list * Proof.context| \\
+  \indexml{Assumption.add-assumes}\verb|Assumption.add_assumes: |\isasep\isanewline%
+\verb|  cterm list -> Proof.context -> thm list * Proof.context| \\
   \indexml{Assumption.export}\verb|Assumption.export: bool -> Proof.context -> Proof.context -> thm -> thm| \\
   \end{mldecls}
 
   \begin{description}
 
-  \item \verb|Assumption.export|
+  \item \verb|Assumption.export| represents arbitrary export
+  rules, which is any function of type \verb|bool -> cterm list -> thm -> thm|,
+  where the \verb|bool| indicates goal mode, and the \verb|cterm list| the collection of assumptions to be discharged
+  simultaneously.
 
-  \item \verb|Assumption.assume|~\isa{A} produces a raw assumption
-  \isa{A\ {\isasymturnstile}\ A{\isacharprime}}, where the conclusion \isa{A{\isacharprime}} is in HHF normal
-  form.
-
-  \item \verb|Assumption.add_assumes|~\isa{As} augments the context
-  by plain assumptions that are discharged via \isa{{\isasymLongrightarrow}{\isacharunderscore}intro} or
-  \isa{{\isacharhash}{\isasymLongrightarrow}{\isacharunderscore}intro}, depending on goal mode.  The resulting facts are
-  hypothetical theorems as produced by \verb|Assumption.assume|.
+  \item \verb|Assumption.assume|~\isa{A} turns proposition \isa{A} into a raw assumption \isa{A\ {\isasymturnstile}\ A{\isacharprime}}, where the conclusion
+  \isa{A{\isacharprime}} is in HHF normal form.
 
   \item \verb|Assumption.add_assms|~\isa{e\ As} augments the context
-  by generic assumptions that are discharged via rule \isa{e}.
+  by assumptions \isa{As} with export rule \isa{e}.  The
+  resulting facts are hypothetical theorems as produced by \verb|Assumption.assume|.
+
+  \item \verb|Assumption.add_assumes|~\isa{As} is a special case of
+  \verb|Assumption.add_assms| where the export rule performs \isa{{\isasymLongrightarrow}{\isacharunderscore}intro} or \isa{{\isacharhash}{\isasymLongrightarrow}{\isacharunderscore}intro}, depending on goal mode.
 
   \item \verb|Assumption.export|~\isa{is{\isacharunderscore}goal\ inner\ outer\ th}
   exports result \isa{th} from the the \isa{inner} context
-  back into the \isa{outer} one.  The \isa{is{\isacharunderscore}goal} flag is
-  \isa{true} for goal mode.  The result is in HHF normal form.
+  back into the \isa{outer} one; \isa{is{\isacharunderscore}goal\ {\isacharequal}\ true} means
+  this is a goal context.  The result is in HHF normal form.  Note
+  that \verb|ProofContext.export| combines \verb|Variable.export|
+  and \verb|Assumption.export| in the canonical way.
 
   \end{description}%
 \end{isamarkuptext}%




