src/HOL/Main.thy
author haftmann
Thu Jun 26 10:06:54 2008 +0200 (2008-06-26)
changeset 27367 a75d71c73362
parent 26729 43a72d892594
child 28091 50f2d6ba024c
permissions -rw-r--r--
added dummy citiation
webertj@17602
     1
(*  Title:      HOL/Main.thy
webertj@17602
     2
    ID:         $Id$
webertj@17602
     3
*)
wenzelm@9619
     4
wenzelm@12024
     5
header {* Main HOL *}
wenzelm@12024
     6
nipkow@15131
     7
theory Main
haftmann@27367
     8
imports Plain Map Presburger Recdef
nipkow@15131
     9
begin
wenzelm@9650
    10
wenzelm@25223
    11
ML {* val HOL_proofs = ! Proofterm.proofs *}
wenzelm@23165
    12
haftmann@27367
    13
text {* See further \cite{Nipkow-et-al:2002:tutorial} *}
haftmann@25964
    14
wenzelm@9650
    15
end