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