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