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}%