# HG changeset patch # User wenzelm # Date 1152197379 -7200 # Node ID 413d4224269b8d19397808fa7494b675fa445596 # Parent 3469df62fe2176d413b919142d09200741438bbb updated; diff -r 3469df62fe21 -r 413d4224269b doc-src/IsarImplementation/Thy/document/integration.tex --- 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% diff -r 3469df62fe21 -r 413d4224269b doc-src/IsarImplementation/Thy/document/proof.tex --- 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}%