src/HOL/Main.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Main.thy	Sun Apr 23 14:15:09 2017 +0200
@@ -0,0 +1,12 @@
+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