src/HOL/Main.thy
author paulson <lp15@cam.ac.uk>
Tue Apr 25 16:39:54 2017 +0100 (2017-04-25)
changeset 65578 e4997c181cce
parent 65553 006a274cdbc2
child 65813 bdd17b18e103
permissions -rw-r--r--
New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
wenzelm@65553
     1
section \<open>Main HOL\<close>
wenzelm@65553
     2
wenzelm@65553
     3
text \<open>
wenzelm@65553
     4
  Classical Higher-order Logic -- only ``Main'', excluding real and
wenzelm@65553
     5
  complex numbers etc.
wenzelm@65553
     6
\<close>
wenzelm@65553
     7
wenzelm@65553
     8
theory Main
wenzelm@65553
     9
imports Pre_Main GCD Binomial
wenzelm@65553
    10
begin
wenzelm@65553
    11
wenzelm@65553
    12
end