# HG changeset patch
# User wenzelm
# Date 1492949709 -7200
# Node ID 006a274cdbc2140a4be4112165822dd4f6423b6f
# Parent  f533820e7248d41d58de00fd57a30e94fcc0a5b0
added missing file (amending f533820e7248);

diff -r f533820e7248 -r 006a274cdbc2 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