1 header {* Main HOL *}
2
3 theory Main
4 imports Plain Predicate_Compile Nitpick
5 begin
6
7 text {*
8 Classical Higher-order Logic -- only ``Main'', excluding real and
9 complex numbers etc.
10 *}
11
12 text {* See further \cite{Nipkow-et-al:2002:tutorial} *}
13
14 end