changeset 65553 | 006a274cdbc2 |
child 65813 | bdd17b18e103 |
--- /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