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