author | wenzelm |
Sun, 23 Apr 2017 14:15:09 +0200 | |
changeset 65553 | 006a274cdbc2 |
parent 65552 | f533820e7248 |
child 65554 | a04afc400156 |
src/HOL/Main.thy | file | annotate | diff | comparison | revisions |
--- /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