src/HOL/Main.thy

--- a/src/HOL/Main.thy	Thu Jan 01 23:31:59 2009 +0100
+++ b/src/HOL/Main.thy	Fri Jan 02 00:21:59 2009 +0100
@@ -1,13 +1,14 @@
-(*  Title:      HOL/Main.thy
-    ID:         $Id$
-*)
-
 header {* Main HOL *}
 
 theory Main
 imports Plain Code_Eval Map Nat_Int_Bij Recdef
 begin
 
+text {*
+  Classical Higher-order Logic -- only ``Main'', excluding real and
+  complex numbers etc.
+*}
+
 text {* See further \cite{Nipkow-et-al:2002:tutorial} *}
 
 end