src/HOL/Main.thy

suppress "Pure" with its special threads=1 (Jenkins log does not provide threads in ISABELLE_BUILD_OPTIONS);

section \<open>Main HOL\<close>

text \<open>
  Classical Higher-order Logic -- only ``Main'', excluding real and
  complex numbers etc.
\<close>

theory Main
imports Pre_Main GCD Binomial
begin

end