wenzelm@12024: header {* Main HOL *}
wenzelm@12024: 
nipkow@15131: theory Main
boehmes@36899: imports Plain Predicate_Compile Nitpick SMT
nipkow@15131: begin
wenzelm@9650: 
wenzelm@29304: text {*
wenzelm@29304:   Classical Higher-order Logic -- only ``Main'', excluding real and
wenzelm@29304:   complex numbers etc.
wenzelm@29304: *}
wenzelm@29304: 
haftmann@27367: text {* See further \cite{Nipkow-et-al:2002:tutorial} *}
haftmann@25964: 
wenzelm@9650: end