theory Syntax imports Base begin chapter {* Concrete syntax and type-checking *} text FIXME section {* Parsing and printing *} text FIXME section {* Checking and unchecking \label{sec:term-check} *} end