src/HOL/Main.thy
changeset 29304 5c71a6da989d
parent 28263 69eaa97e7e96
child 29820 07f53494cf20
     1.1 --- a/src/HOL/Main.thy	Thu Jan 01 23:31:59 2009 +0100
     1.2 +++ b/src/HOL/Main.thy	Fri Jan 02 00:21:59 2009 +0100
     1.3 @@ -1,13 +1,14 @@
     1.4 -(*  Title:      HOL/Main.thy
     1.5 -    ID:         $Id$
     1.6 -*)
     1.7 -
     1.8  header {* Main HOL *}
     1.9  
    1.10  theory Main
    1.11  imports Plain Code_Eval Map Nat_Int_Bij Recdef
    1.12  begin
    1.13  
    1.14 +text {*
    1.15 +  Classical Higher-order Logic -- only ``Main'', excluding real and
    1.16 +  complex numbers etc.
    1.17 +*}
    1.18 +
    1.19  text {* See further \cite{Nipkow-et-al:2002:tutorial} *}
    1.20  
    1.21  end