# HG changeset patch
# User wenzelm
# Date 1152356067 -7200
# Node ID ae7aba935986d3d7be734a9d6dc210bbf0eeb84e
# Parent  02c59ec2f2e16e9c47ecb36716eb3963a142ae60
added some bits on variables;

diff -r 02c59ec2f2e1 -r ae7aba935986 doc-src/IsarImplementation/Thy/proof.thy
--- a/doc-src/IsarImplementation/Thy/proof.thy	Sat Jul 08 12:54:26 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/proof.thy	Sat Jul 08 12:54:27 2006 +0200
@@ -21,18 +21,31 @@
 
   \begin{description}
 
-  \item @{ML Variable.declare_term} FIXME
+  \item @{ML 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 @{ML Variable.import} FIXME
+  \item @{ML Variable.import} introduces new fixes for schematic type
+  and term variables occurring in given facts.  The effect may be
+  reversed (up to renaming) via @{ML Variable.export}.
 
-  \item @{ML Variable.export} FIXME
+  \item @{ML 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 @{ML Variable.trade} composes @{ML Variable.import} and @{ML
-  Variable.export}.
+  Variable.export}, i.e.\ it provides a view on facts with all
+  variables being fixed in the current context.
 
-  \item @{ML Variable.monomorphic} FIXME
+  \item @{ML Variable.monomorphic} introduces fixed type variables for
+  the schematic of the given facts.
 
-  \item @{ML Variable.polymorphic} FIXME
+  \item @{ML 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}
 *}