src/HOL/Main.thy
author wenzelm
Sat, 13 Mar 2010 14:44:47 +0100
changeset 35743 c506c029a082
parent 35284 9edc2bd6d2bd
child 36899 bcd6fce5bf06
permissions -rw-r--r--
adapted to localized typedef: handle single global interpretation only;

header {* Main HOL *}

theory Main
imports Plain Predicate_Compile Nitpick
begin

text {*
  Classical Higher-order Logic -- only ``Main'', excluding real and
  complex numbers etc.
*}

text {* See further \cite{Nipkow-et-al:2002:tutorial} *}

end