src/HOL/Main.thy
changeset 29304 5c71a6da989d
parent 28263 69eaa97e7e96
child 29820 07f53494cf20
equal deleted inserted replaced
29303:57f0d287375e 29304:5c71a6da989d
     1 (*  Title:      HOL/Main.thy
       
     2     ID:         $Id$
       
     3 *)
       
     4 
       
     5 header {* Main HOL *}
     1 header {* Main HOL *}
     6 
     2 
     7 theory Main
     3 theory Main
     8 imports Plain Code_Eval Map Nat_Int_Bij Recdef
     4 imports Plain Code_Eval Map Nat_Int_Bij Recdef
     9 begin
     5 begin
    10 
     6 
       
     7 text {*
       
     8   Classical Higher-order Logic -- only ``Main'', excluding real and
       
     9   complex numbers etc.
       
    10 *}
       
    11 
    11 text {* See further \cite{Nipkow-et-al:2002:tutorial} *}
    12 text {* See further \cite{Nipkow-et-al:2002:tutorial} *}
    12 
    13 
    13 end
    14 end