doc-src/IsarImplementation/Thy/document/Isar.tex

--- a/doc-src/IsarImplementation/Thy/document/Isar.tex	Mon Feb 16 21:39:19 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Isar.tex	Mon Feb 16 21:39:52 2009 +0100
@@ -18,11 +18,27 @@
 %
 \endisadelimtheory
 %
-\isamarkupchapter{Isar proof texts%
+\isamarkupchapter{Isar language elements%
 }
 \isamarkuptrue%
 %
-\isamarkupsection{Proof context%
+\begin{isamarkuptext}%
+The primary Isar language consists of three main categories of
+  language elements:
+
+  \begin{enumerate}
+
+  \item Proof commands
+
+  \item Proof methods
+
+  \item Attributes
+
+  \end{enumerate}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Proof commands%
 }
 \isamarkuptrue%
 %
@@ -31,26 +47,6 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsection{Proof state \label{sec:isar-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{Proof methods%
 }
 \isamarkuptrue%
@@ -65,7 +61,7 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-FIXME ?!%
+FIXME%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %