diff -r d7ad1217c24a -r 05fd007bdeb9 doc-src/IsarImplementation/Thy/document/isar.tex
--- a/doc-src/IsarImplementation/Thy/document/isar.tex	Tue Sep 12 17:23:34 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/isar.tex	Tue Sep 12 17:45:58 2006 +0200
@@ -23,7 +23,16 @@
 }
 \isamarkuptrue%
 %
-\isamarkupsection{Proof states \label{sec:isar-proof-state}%
+\isamarkupsection{Proof context%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Proof state \label{sec:isar-proof-state}%
 }
 \isamarkuptrue%
 %