doc-src/IsarImplementation/Thy/Syntax.thy

--- a/doc-src/IsarImplementation/Thy/Syntax.thy	Fri Jan 29 23:57:57 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/Syntax.thy	Fri Jan 29 23:59:03 2010 +0100
@@ -2,8 +2,14 @@
 imports Base
 begin
 
-chapter {* Syntax and type-checking *}
+chapter {* Concrete syntax and type-checking *}
 
 text FIXME
 
+section {* Parsing and printing *}
+
+text FIXME
+
+section {* Checking and unchecking \label{sec:term-check} *}
+
 end