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