--- a/doc-src/IsarImplementation/Thy/proof.thy Thu Jul 06 16:49:37 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/proof.thy Thu Jul 06 16:49:38 2006 +0200
@@ -7,6 +7,36 @@
section {* Proof context *}
+subsection {* Local variables *}
+
+text %mlref {*
+ \begin{mldecls}
+ @{index_ML Variable.declare_term: "term -> Proof.context -> 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"} \\
+ @{index_ML Variable.monomorphic: "Proof.context -> term list -> term list"} \\
+ @{index_ML Variable.polymorphic: "Proof.context -> term list -> term list"} \\
+ \end{mldecls}
+
+ \begin{description}
+
+ \item @{ML Variable.declare_term} FIXME
+
+ \item @{ML Variable.import} FIXME
+
+ \item @{ML Variable.export} FIXME
+
+ \item @{ML Variable.trade} composes @{ML Variable.import} and @{ML
+ Variable.export}.
+
+ \item @{ML Variable.monomorphic} FIXME
+
+ \item @{ML Variable.polymorphic} FIXME
+
+ \end{description}
+*}
+
text FIXME
section {* Proof state *}