src/HOL/Main.thy

+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