1.1 --- a/doc-src/IsarImplementation/Thy/document/integration.tex Sat Jul 08 14:01:31 2006 +0200
1.2 +++ b/doc-src/IsarImplementation/Thy/document/integration.tex Sat Jul 08 14:01:40 2006 +0200
1.3 @@ -356,7 +356,7 @@
1.4 toplevel state and optional error condition, respectively. This
1.5 only works after dropping out of the Isar toplevel loop.
1.6
1.7 - \item \verb|Isar.context ()| produces the proof context from \verb|Isar.state ()| above.
1.8 + \item \verb|Isar.context ()| produces the proof context from \verb|Isar.state ()|.
1.9
1.10 \end{description}%
1.11 \end{isamarkuptext}%
2.1 --- a/doc-src/IsarImplementation/Thy/integration.thy Sat Jul 08 14:01:31 2006 +0200
2.2 +++ b/doc-src/IsarImplementation/Thy/integration.thy Sat Jul 08 14:01:40 2006 +0200
2.3 @@ -293,7 +293,7 @@
2.4 only works after dropping out of the Isar toplevel loop.
2.5
2.6 \item @{ML "Isar.context ()"} produces the proof context from @{ML
2.7 - "Isar.state ()"} above.
2.8 + "Isar.state ()"}.
2.9
2.10 \end{description}
2.11 *}
3.1 --- a/doc-src/IsarImplementation/Thy/proof.thy Sat Jul 08 14:01:31 2006 +0200
3.2 +++ b/doc-src/IsarImplementation/Thy/proof.thy Sat Jul 08 14:01:40 2006 +0200
3.3 @@ -9,9 +9,12 @@
3.4
3.5 subsection {* Local variables *}
3.6
3.7 +text FIXME
3.8 +
3.9 text %mlref {*
3.10 \begin{mldecls}
3.11 @{index_ML Variable.declare_term: "term -> Proof.context -> Proof.context"} \\
3.12 + @{index_ML Variable.add_fixes: "string list -> Proof.context -> string list * Proof.context"} \\
3.13 @{index_ML Variable.import: "bool -> thm list -> Proof.context -> thm list * Proof.context"} \\
3.14 @{index_ML Variable.export: "Proof.context -> Proof.context -> thm list -> thm list"} \\
3.15 @{index_ML Variable.trade: "Proof.context -> (thm list -> thm list) -> thm list -> thm list"} \\
3.16 @@ -21,31 +24,46 @@
3.17
3.18 \begin{description}
3.19
3.20 - \item @{ML Variable.declare_term} declares a term as belonging to
3.21 - the current context. This fixes free type variables, but not term
3.22 - variables; constraints for type and term variables are declared
3.23 - uniformly.
3.24 + \item @{ML Variable.declare_term}~@{text "t ctxt"} declares term
3.25 + @{text "t"} to belong to the context. This fixes free type
3.26 + variables, but not term variables. Constraints for type and term
3.27 + variables are declared uniformly.
3.28
3.29 - \item @{ML Variable.import} introduces new fixes for schematic type
3.30 - and term variables occurring in given facts. The effect may be
3.31 - reversed (up to renaming) via @{ML Variable.export}.
3.32 + \item @{ML Variable.add_fixes}~@{text "xs ctxt"} fixes term
3.33 + variables @{text "xs"} and returns the internal names of the
3.34 + resulting Skolem constants. Note that term fixes refer to
3.35 + \emph{all} type instances that may occur in the future.
3.36
3.37 - \item @{ML Variable.export} generalizes fixed type and term
3.38 - variables according to the difference of the two contexts. Note
3.39 - that type variables occurring in term variables are still fixed,
3.40 - even though they got introduced later (e.g.\ by type-inference).
3.41 + \item @{ML Variable.invent_fixes} is similar to @{ML
3.42 + Variable.add_fixes}, but the given names merely act as hints for
3.43 + internal fixes produced here.
3.44 +
3.45 + \item @{ML Variable.import}~@{text "open ths ctxt"} augments the
3.46 + context by new fixes for the schematic type and term variables
3.47 + occurring in @{text "ths"}. The @{text "open"} flag indicates
3.48 + whether the fixed names should be accessible to the user, otherwise
3.49 + internal names are chosen.
3.50 +
3.51 + \item @{ML Variable.export}~@{text "inner outer ths"} generalizes
3.52 + fixed type and term variables in @{text "ths"} according to the
3.53 + difference of the @{text "inner"} and @{text "outer"} context. Note
3.54 + that type variables occurring in term variables are still fixed.
3.55 +
3.56 + @{ML Variable.export} essentially reverses the effect of @{ML
3.57 + Variable.import} (up to renaming of schematic variables.
3.58
3.59 \item @{ML Variable.trade} composes @{ML Variable.import} and @{ML
3.60 Variable.export}, i.e.\ it provides a view on facts with all
3.61 variables being fixed in the current context.
3.62
3.63 - \item @{ML Variable.monomorphic} introduces fixed type variables for
3.64 - the schematic of the given facts.
3.65 + \item @{ML Variable.monomorphic}~@{text "ctxt ts"} introduces fixed
3.66 + type variables for the schematic ones in @{text "ts"}.
3.67
3.68 - \item @{ML Variable.polymorphic} generalizes type variables as far
3.69 - as possible, even those occurring in fixed term variables. This
3.70 - operation essentially reverses the default policy of type-inference
3.71 - to introduce local polymorphism entities in fixed form.
3.72 + \item @{ML Variable.polymorphic}~@{text "ctxt ts"} generalizes type
3.73 + variables in @{text "ts"} as far as possible, even those occurring
3.74 + in fixed term variables. This operation essentially reverses the
3.75 + default policy of type-inference to introduce local polymorphism as
3.76 + fixed types.
3.77
3.78 \end{description}
3.79 *}
4.1 --- a/doc-src/IsarImplementation/implementation.tex Sat Jul 08 14:01:31 2006 +0200
4.2 +++ b/doc-src/IsarImplementation/implementation.tex Sat Jul 08 14:01:40 2006 +0200
4.3 @@ -50,7 +50,7 @@
4.4
4.5 {\small\em As I did 20 years ago, I still fervently believe that the
4.6 only way to make software secure, reliable, and fast is to make it
4.7 - small. Fight Features.}
4.8 + small. Fight features.}
4.9
4.10 Andrew S. Tanenbaum
4.11