src/HOL/Main.thy
author wenzelm
Sun, 23 Apr 2017 14:15:09 +0200
changeset 65553 006a274cdbc2
child 65813 bdd17b18e103
permissions -rw-r--r--
added missing file (amending f533820e7248);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
65553
006a274cdbc2 added missing file (amending f533820e7248);
wenzelm
parents:
diff changeset
     1
section \<open>Main HOL\<close>
006a274cdbc2 added missing file (amending f533820e7248);
wenzelm
parents:
diff changeset
     2
006a274cdbc2 added missing file (amending f533820e7248);
wenzelm
parents:
diff changeset
     3
text \<open>
006a274cdbc2 added missing file (amending f533820e7248);
wenzelm
parents:
diff changeset
     4
  Classical Higher-order Logic -- only ``Main'', excluding real and
006a274cdbc2 added missing file (amending f533820e7248);
wenzelm
parents:
diff changeset
     5
  complex numbers etc.
006a274cdbc2 added missing file (amending f533820e7248);
wenzelm
parents:
diff changeset
     6
\<close>
006a274cdbc2 added missing file (amending f533820e7248);
wenzelm
parents:
diff changeset
     7
006a274cdbc2 added missing file (amending f533820e7248);
wenzelm
parents:
diff changeset
     8
theory Main
006a274cdbc2 added missing file (amending f533820e7248);
wenzelm
parents:
diff changeset
     9
imports Pre_Main GCD Binomial
006a274cdbc2 added missing file (amending f533820e7248);
wenzelm
parents:
diff changeset
    10
begin
006a274cdbc2 added missing file (amending f533820e7248);
wenzelm
parents:
diff changeset
    11
006a274cdbc2 added missing file (amending f533820e7248);
wenzelm
parents:
diff changeset
    12
end