replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
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