added some bits on variables;
Sat, 08 Jul 2006 12:54:27 +0200
changeset 20041 ae7aba935986
parent 20040 02c59ec2f2e1
child 20042 2308529f8e8d
added some bits on variables;
--- 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 @@
-  \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} 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.