diff -r 725a91601ed1 -r 27ea2ba48fa3 doc-src/IsarImplementation/Thy/document/proof.tex
--- a/doc-src/IsarImplementation/Thy/document/proof.tex	Thu Aug 31 18:27:40 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/proof.tex	Thu Aug 31 22:55:49 2006 +0200
@@ -19,15 +19,11 @@
 %
 \endisadelimtheory
 %
-\isamarkupchapter{Structured reasoning%
+\isamarkupchapter{Structured proofs%
 }
 \isamarkuptrue%
 %
-\isamarkupsection{Proof context%
-}
-\isamarkuptrue%
-%
-\isamarkupsubsection{Local variables%
+\isamarkupsection{Local variables%
 }
 \isamarkuptrue%
 %
@@ -105,7 +101,34 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsection{Proof state%
+\isamarkupsection{Schematic polymorphism%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Assumptions%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Conclusions%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Structured proofs \label{sec:isar-proof-state}%
 }
 \isamarkuptrue%
 %
@@ -125,7 +148,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsection{Methods%
+\isamarkupsection{Proof methods%
 }
 \isamarkuptrue%
 %
@@ -139,7 +162,7 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-FIXME%
+FIXME ?!%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %