doc-src/IsarImplementation/Thy/proof.thy

--- a/doc-src/IsarImplementation/Thy/proof.thy	Sat Jul 08 14:01:31 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/proof.thy	Sat Jul 08 14:01:40 2006 +0200
@@ -9,9 +9,12 @@
 
 subsection {* Local variables *}
 
+text FIXME
+
 text %mlref {*
   \begin{mldecls}
   @{index_ML Variable.declare_term: "term -> Proof.context -> Proof.context"} \\
+  @{index_ML Variable.add_fixes: "string list -> Proof.context -> string list * Proof.context"} \\
   @{index_ML Variable.import: "bool -> thm list -> Proof.context -> thm list * Proof.context"} \\
   @{index_ML Variable.export: "Proof.context -> Proof.context -> thm list -> thm list"} \\
   @{index_ML Variable.trade: "Proof.context -> (thm list -> thm list) -> thm list -> thm list"} \\
@@ -21,31 +24,46 @@
 
   \begin{description}
 
-  \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.declare_term}~@{text "t ctxt"} declares term
+  @{text "t"} to belong to the context.  This fixes free type
+  variables, but not term variables.  Constraints for type and term
+  variables are declared uniformly.
+
+  \item @{ML Variable.add_fixes}~@{text "xs ctxt"} fixes term
+  variables @{text "xs"} and returns the internal names of the
+  resulting Skolem constants.  Note that term fixes refer to
+  \emph{all} type instances that may occur in the future.
+
+  \item @{ML Variable.invent_fixes} is similar to @{ML
+  Variable.add_fixes}, but the given names merely act as hints for
+  internal fixes produced here.
 
-  \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.import}~@{text "open ths ctxt"} augments the
+  context by new fixes for the schematic type and term variables
+  occurring in @{text "ths"}.  The @{text "open"} flag indicates
+  whether the fixed names should be accessible to the user, otherwise
+  internal names are chosen.
 
-  \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.export}~@{text "inner outer ths"} generalizes
+  fixed type and term variables in @{text "ths"} according to the
+  difference of the @{text "inner"} and @{text "outer"} context.  Note
+  that type variables occurring in term variables are still fixed.
+
+  @{ML Variable.export} essentially reverses the effect of @{ML
+  Variable.import} (up to renaming of schematic variables.
 
   \item @{ML Variable.trade} composes @{ML Variable.import} and @{ML
   Variable.export}, i.e.\ it provides a view on facts with all
   variables being fixed in the current context.
 
-  \item @{ML Variable.monomorphic} introduces fixed type variables for
-  the schematic of the given facts.
+  \item @{ML Variable.monomorphic}~@{text "ctxt ts"} introduces fixed
+  type variables for the schematic ones in @{text "ts"}.
 
-  \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.
+  \item @{ML Variable.polymorphic}~@{text "ctxt ts"} generalizes type
+  variables in @{text "ts"} 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 as
+  fixed types.
 
   \end{description}
 *}