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
     1 (*  Title:      HOL/Main.thy
     2     ID:         $Id$
     3 *)
     4 
     5 header {* Main HOL *}
     6 
     7 theory Main
     8 imports Plain Map Presburger Recdef
     9 begin
    10 
    11 ML {* val HOL_proofs = ! Proofterm.proofs *}
    12 
    13 text {* See further \cite{Nipkow-et-al:2002:tutorial} *}
    14 
    15 end