--- a/doc-src/IsarImplementation/Thy/document/integration.tex Thu Jul 06 16:49:38 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/integration.tex Thu Jul 06 16:49:39 2006 +0200
@@ -58,9 +58,8 @@
\isa{theory}, or \isa{proof}. On entering the main Isar loop we
start with an empty toplevel. A theory is commenced by giving a
\isa{{\isasymTHEORY}} header; within a theory we may issue theory
- commands such as \isa{{\isasymCONSTS}} or \isa{{\isasymDEFS}}, or state a
- \isa{{\isasymTHEOREM}} to be proven. Now we are within a proof state,
- with a rich collection of Isar proof commands for structured proof
+ commands such as \isa{{\isasymDEFINITION}}, or state a \isa{{\isasymTHEOREM}} to be proven. Now we are within a proof state, with a
+ rich collection of Isar proof commands for structured proof
composition, or unstructured proof scripts. When the proof is
concluded we get back to the theory, which is then updated by
storing the resulting fact. Further theory declarations or theorem
@@ -341,6 +340,7 @@
\indexml{Isar.main}\verb|Isar.main: unit -> unit| \\
\indexml{Isar.loop}\verb|Isar.loop: unit -> unit| \\
\indexml{Isar.state}\verb|Isar.state: unit -> Toplevel.state| \\
+ \indexml{Isar.context}\verb|Isar.context: unit -> Proof.context| \\
\indexml{Isar.exn}\verb|Isar.exn: unit -> (exn * string) option| \\
\end{mldecls}
@@ -356,6 +356,8 @@
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.
+
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
--- a/doc-src/IsarImplementation/Thy/document/proof.tex Thu Jul 06 16:49:38 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/proof.tex Thu Jul 06 16:49:39 2006 +0200
@@ -27,6 +27,51 @@
}
\isamarkuptrue%
%
+\isamarkupsubsection{Local variables%
+}
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+ \indexml{Variable.declare-term}\verb|Variable.declare_term: term -> Proof.context -> 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| \\
+ \indexml{Variable.monomorphic}\verb|Variable.monomorphic: Proof.context -> term list -> term list| \\
+ \indexml{Variable.polymorphic}\verb|Variable.polymorphic: Proof.context -> term list -> term list| \\
+ \end{mldecls}
+
+ \begin{description}
+
+ \item \verb|Variable.declare_term| FIXME
+
+ \item \verb|Variable.import| FIXME
+
+ \item \verb|Variable.export| FIXME
+
+ \item \verb|Variable.trade| composes \verb|Variable.import| and \verb|Variable.export|.
+
+ \item \verb|Variable.monomorphic| FIXME
+
+ \item \verb|Variable.polymorphic| FIXME
+
+ \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
\begin{isamarkuptext}%
FIXME%
\end{isamarkuptext}%