# HG changeset patch
# User wenzelm
# Date 1152356069 -7200
# Node ID 03612801317824925cf436eddcfc93469e1fe05d
# Parent  2308529f8e8dc1aac74b236affdca74c080b1883
updated;

diff -r 2308529f8e8d -r 036128013178 doc-src/IsarImplementation/Thy/document/proof.tex
--- a/doc-src/IsarImplementation/Thy/document/proof.tex	Sat Jul 08 12:54:28 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/proof.tex	Sat Jul 08 12:54:29 2006 +0200
@@ -49,17 +49,30 @@
 
   \begin{description}
 
-  \item \verb|Variable.declare_term| FIXME
+  \item \verb|Variable.declare_term| declares a term as belonging to
+  the current context.  This fixes free type variables, but not term
+  variables; constraints for type and term variables are declared
+  uniformly.
 
-  \item \verb|Variable.import| FIXME
-
-  \item \verb|Variable.export| FIXME
+  \item \verb|Variable.import| introduces new fixes for schematic type
+  and term variables occurring in given facts.  The effect may be
+  reversed (up to renaming) via \verb|Variable.export|.
 
-  \item \verb|Variable.trade| composes \verb|Variable.import| and \verb|Variable.export|.
+  \item \verb|Variable.export| generalizes fixed type and term
+  variables according to the difference of the two contexts.  Note
+  that type variables occurring in term variables are still fixed,
+  even though they got introduced later (e.g.\ by type-inference).
+
+  \item \verb|Variable.trade| composes \verb|Variable.import| and \verb|Variable.export|, i.e.\ it provides a view on facts with all
+  variables being fixed in the current context.
 
-  \item \verb|Variable.monomorphic| FIXME
+  \item \verb|Variable.monomorphic| introduces fixed type variables for
+  the schematic of the given facts.
 
-  \item \verb|Variable.polymorphic| FIXME
+  \item \verb|Variable.polymorphic| generalizes type variables as far
+  as possible, even those occurring in fixed term variables.  This
+  operation essentially reverses the default policy of type-inference
+  to introduce local polymorphism entities in fixed form.
 
   \end{description}%
 \end{isamarkuptext}%
diff -r 2308529f8e8d -r 036128013178 doc-src/IsarImplementation/Thy/document/tactic.tex
--- a/doc-src/IsarImplementation/Thy/document/tactic.tex	Sat Jul 08 12:54:28 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/tactic.tex	Sat Jul 08 12:54:29 2006 +0200
@@ -195,15 +195,17 @@
 %
 \begin{isamarkuptext}%
 \begin{mldecls}
-  \indexml{Goal.prove}\verb|Goal.prove: theory -> string list -> term list -> term ->|\isasep\isanewline%
+  \indexml{Goal.prove}\verb|Goal.prove: Proof.context -> string list -> term list -> term ->|\isasep\isanewline%
 \verb|  (thm list -> tactic) -> thm| \\
-  \indexml{Goal.prove-multi}\verb|Goal.prove_multi: theory -> string list -> term list -> term list ->|\isasep\isanewline%
+  \indexml{Goal.prove-multi}\verb|Goal.prove_multi: Proof.context -> string list -> term list -> term list ->|\isasep\isanewline%
 \verb|  (thm list -> tactic) -> thm list| \\
+  \indexml{Goal.prove-global}\verb|Goal.prove_global: theory -> string list -> term list -> term ->|\isasep\isanewline%
+\verb|  (thm list -> tactic) -> thm| \\
   \end{mldecls}
 
   \begin{description}
 
-  \item \verb|Goal.prove|~\isa{thy\ xs\ As\ C\ tac} states goal \isa{C} in the context of arbitrary-but-fixed parameters \isa{xs}
+  \item \verb|Goal.prove|~\isa{ctxt\ xs\ As\ C\ tac} states goal \isa{C} in the context of arbitrary-but-fixed parameters \isa{xs}
   and hypotheses \isa{As} and applies tactic \isa{tac} to
   solve it.  The latter may depend on the local assumptions being
   presented as facts.  The result is essentially \isa{{\isasymAnd}xs{\isachardot}\ As\ {\isasymLongrightarrow}\ C}, but is normalized by pulling \isa{{\isasymAnd}} before \isa{{\isasymLongrightarrow}}
@@ -219,6 +221,8 @@
   states several conclusions simultaneously.  \verb|Tactic.conjunction_tac| may be used to split these into individual
   subgoals before commencing the actual proof.
 
+  \item \verb|Goal.prove_global| is a degraded version of \verb|Goal.prove| for theory level goals; it includes a global \verb|Drule.standard| for the result.
+
   \end{description}%
 \end{isamarkuptext}%
 \isamarkuptrue%