src/HOL/Main.thy
author blanchet
Mon, 09 Aug 2010 14:08:30 +0200
changeset 38290 581a402a80f0
parent 36899 bcd6fce5bf06
child 38393 7c045c03598f
permissions -rw-r--r--
prevent ATP thread for staying around for 1 minute if an exception occurred earlier; this is a workaround for what could be a misfeature of "Async_Manager", which I'd rather not touch

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