--- a/doc-src/IsarImplementation/Thy/document/integration.tex Sat Jul 08 14:01:31 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/integration.tex Sat Jul 08 14:01:40 2006 +0200
@@ -356,7 +356,7 @@
toplevel state and optional error condition, respectively. This
only works after dropping out of the Isar toplevel loop.
- \item \verb|Isar.context ()| produces the proof context from \verb|Isar.state ()| above.
+ \item \verb|Isar.context ()| produces the proof context from \verb|Isar.state ()|.
\end{description}%
\end{isamarkuptext}%
--- a/doc-src/IsarImplementation/Thy/integration.thy Sat Jul 08 14:01:31 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/integration.thy Sat Jul 08 14:01:40 2006 +0200
@@ -293,7 +293,7 @@
only works after dropping out of the Isar toplevel loop.
\item @{ML "Isar.context ()"} produces the proof context from @{ML
- "Isar.state ()"} above.
+ "Isar.state ()"}.
\end{description}
*}
--- 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}
*}
--- a/doc-src/IsarImplementation/implementation.tex Sat Jul 08 14:01:31 2006 +0200
+++ b/doc-src/IsarImplementation/implementation.tex Sat Jul 08 14:01:40 2006 +0200
@@ -50,7 +50,7 @@
{\small\em As I did 20 years ago, I still fervently believe that the
only way to make software secure, reliable, and fast is to make it
- small. Fight Features.}
+ small. Fight features.}
Andrew S. Tanenbaum