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