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
     1 section \<open>Main HOL\<close>
     2 
     3 text \<open>
     4   Classical Higher-order Logic -- only ``Main'', excluding real and
     5   complex numbers etc.
     6 \<close>
     7 
     8 theory Main
     9 imports Pre_Main GCD Binomial
    10 begin
    11 
    12 end