--- 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