diff -r ab23493e1f0f -r 31f8d9eaceff doc-src/IsarImplementation/Thy/document/Syntax.tex
--- a/doc-src/IsarImplementation/Thy/document/Syntax.tex	Fri Feb 05 11:51:52 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Syntax.tex	Fri Feb 05 14:39:02 2010 +0100
@@ -18,7 +18,7 @@
 %
 \endisadelimtheory
 %
-\isamarkupchapter{Syntax and type-checking%
+\isamarkupchapter{Concrete syntax and type-checking%
 }
 \isamarkuptrue%
 %
@@ -27,6 +27,19 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
+\isamarkupsection{Parsing and printing%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Checking and unchecking \label{sec:term-check}%
+}
+\isamarkuptrue%
+%
 \isadelimtheory
 %
 \endisadelimtheory