--- a/doc-src/IsarImplementation/Thy/document/proof.tex Fri Sep 01 20:40:05 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/proof.tex Fri Sep 01 20:44:16 2006 +0200
@@ -23,7 +23,7 @@
}
\isamarkuptrue%
%
-\isamarkupsection{Variables and schematic polymorphism%
+\isamarkupsection{Variables%
}
\isamarkuptrue%
%
@@ -45,7 +45,6 @@
\indexml{Variable.import}\verb|Variable.import: bool ->|\isasep\isanewline%
\verb| thm list -> Proof.context -> ((ctyp list * cterm list) * 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| \\
\indexml{Variable.polymorphic}\verb|Variable.polymorphic: Proof.context -> term list -> term list| \\
\end{mldecls}
@@ -77,9 +76,6 @@
\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.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
--- a/doc-src/IsarImplementation/Thy/proof.thy Fri Sep 01 20:40:05 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/proof.thy Fri Sep 01 20:44:16 2006 +0200
@@ -5,7 +5,7 @@
chapter {* Structured proofs *}
-section {* Variables and schematic polymorphism *}
+section {* Variables *}
text FIXME
@@ -16,7 +16,6 @@
@{index_ML Variable.import: "bool ->
thm list -> Proof.context -> ((ctyp list * cterm list) * 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"} \\
@{index_ML Variable.polymorphic: "Proof.context -> term list -> term list"} \\
\end{mldecls}
@@ -50,10 +49,6 @@
@{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.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
--- a/doc-src/IsarImplementation/Thy/unused.thy Fri Sep 01 20:40:05 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/unused.thy Fri Sep 01 20:44:16 2006 +0200
@@ -1,5 +1,15 @@
text {*
+
+ @{index_ML Variable.trade: "Proof.context -> (thm list -> thm list) -> thm list -> thm list"} \\
+
+
+
+ \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.
+
+
In practice, super-contexts emerge either by merging existing ones,
or by adding explicit declarations. For example, new theories are
usually derived by importing existing theories from the library