# HG changeset patch
# User wenzelm
# Date 1152360091 -7200
# Node ID d8d9ea6a6b559a53f0bfecf7bffaa960088a845d
# Parent  60de4603e6451716d6a835d59dde991aed4cdaee
updated;

diff -r 60de4603e645 -r d8d9ea6a6b55 doc-src/IsarImplementation/Thy/document/proof.tex
--- a/doc-src/IsarImplementation/Thy/document/proof.tex	Sat Jul 08 12:54:50 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/proof.tex	Sat Jul 08 14:01:31 2006 +0200
@@ -31,6 +31,11 @@
 }
 \isamarkuptrue%
 %
+\begin{isamarkuptext}%
+FIXME%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
 \isadelimmlref
 %
 \endisadelimmlref
@@ -40,6 +45,7 @@
 \begin{isamarkuptext}%
 \begin{mldecls}
   \indexml{Variable.declare-term}\verb|Variable.declare_term: term -> Proof.context -> Proof.context| \\
+  \indexml{Variable.add-fixes}\verb|Variable.add_fixes: string list -> Proof.context -> string list * Proof.context| \\
   \indexml{Variable.import}\verb|Variable.import: bool -> thm list -> Proof.context -> thm list * Proof.context| \\
   \indexml{Variable.export}\verb|Variable.export: Proof.context -> Proof.context -> thm list -> thm list| \\
   \indexml{Variable.trade}\verb|Variable.trade: Proof.context -> (thm list -> thm list) -> thm list -> thm list| \\
@@ -49,30 +55,43 @@
 
   \begin{description}
 
-  \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.declare_term|~\isa{t\ ctxt} declares term
+  \isa{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 \verb|Variable.add_fixes|~\isa{xs\ ctxt} fixes term
+  variables \isa{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 \verb|Variable.invent_fixes| is similar to \verb|Variable.add_fixes|, but the given names merely act as hints for
+  internal fixes produced here.
 
-  \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.import|~\isa{open\ ths\ ctxt} augments the
+  context by new fixes for the schematic type and term variables
+  occurring in \isa{ths}.  The \isa{open} flag indicates
+  whether the fixed names should be accessible to the user, otherwise
+  internal names are chosen.
 
-  \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.export|~\isa{inner\ outer\ ths} generalizes
+  fixed type and term variables in \isa{ths} according to the
+  difference of the \isa{inner} and \isa{outer} context.  Note
+  that type variables occurring in term variables are still fixed.
+
+  \verb|Variable.export| essentially reverses the effect of \verb|Variable.import| (up to renaming of schematic variables.
 
   \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| introduces fixed type variables for
-  the schematic of the given facts.
+  \item \verb|Variable.monomorphic|~\isa{ctxt\ ts} introduces fixed
+  type variables for the schematic ones in \isa{ts}.
 
-  \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.
+  \item \verb|Variable.polymorphic|~\isa{ctxt\ ts} generalizes type
+  variables in \isa{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}%
 \end{isamarkuptext}%