header {* Main HOL *} theory Main imports Plain Predicate_Compile Nitpick SMT begin text {* Classical Higher-order Logic -- only ``Main'', excluding real and complex numbers etc. *} text {* See further \cite{Nipkow-et-al:2002:tutorial} *} end