--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarImplementation/Thy/document/proof.tex	Mon Jan 02 20:16:52 2006 +0100
@@ -0,0 +1,91 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{proof}%
+%
+\isadelimtheory
+\isanewline
+\isanewline
+\isanewline
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{theory}\isamarkupfalse%
+\ {\isachardoublequoteopen}proof{\isachardoublequoteclose}\ \isakeyword{imports}\ base\ \isakeyword{begin}%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isamarkupchapter{Structured reasoning%
+}
+\isamarkuptrue%
+%
+\isamarkupsection{Proof context%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Proof state%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME
+
+\glossary{Proof state}{The whole configuration of a structured proof,
+consisting of a \seeglossary{proof context} and an optional
+\seeglossary{structured goal}.  Internally, an Isar proof state is
+organized as a stack to accomodate block structure of proof texts.
+For historical reasons, a low-level \seeglossary{tactical goal} is
+occasionally called ``proof state'' as well.}
+
+\glossary{Structured goal}{FIXME}
+
+\glossary{Goal}{See \seeglossary{tactical goal} or \seeglossary{structured goal}. \norefpage}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Methods%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Attributes%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{end}\isamarkupfalse%
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+\isanewline
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End: