# HG changeset patch
# User wenzelm
# Date 1230852119 -3600
# Node ID 5c71a6da989d04b1f7d0bab4bc4df73eed8d3dbc
# Parent  57f0d287375ee9cfc380c8eb550ad892ac115255
tuned header and description of boot files;

diff -r 57f0d287375e -r 5c71a6da989d src/HOL/Complex_Main.thy
--- a/src/HOL/Complex_Main.thy	Thu Jan 01 23:31:59 2009 +0100
+++ b/src/HOL/Complex_Main.thy	Fri Jan 02 00:21:59 2009 +0100
@@ -1,9 +1,4 @@
-(*  Title:      HOL/Complex_Main.thy
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   2003  University of Cambridge
-*)
-
-header{*Comprehensive Complex Theory*}
+header {* Comprehensive Complex Theory *}
 
 theory Complex_Main
 imports
diff -r 57f0d287375e -r 5c71a6da989d 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
diff -r 57f0d287375e -r 5c71a6da989d src/HOL/Plain.thy
--- a/src/HOL/Plain.thy	Thu Jan 01 23:31:59 2009 +0100
+++ b/src/HOL/Plain.thy	Fri Jan 02 00:21:59 2009 +0100
@@ -1,15 +1,14 @@
-(*  Title:      HOL/Plain.thy
-    ID:         $Id$
-
-Contains fundamental HOL tools and packages.  Does not include Hilbert_Choice.
-*)
-
 header {* Plain HOL *}
 
 theory Plain
 imports Datatype FunDef Record SAT Extraction
 begin
 
+text {*
+  Plain bootstrap of fundamental HOL tools and packages; does not
+  include @{text Hilbert_Choice}.
+*}
+
 ML {* path_add "~~/src/HOL/Library" *}
 
 end
diff -r 57f0d287375e -r 5c71a6da989d src/HOL/ROOT.ML
--- a/src/HOL/ROOT.ML	Thu Jan 01 23:31:59 2009 +0100
+++ b/src/HOL/ROOT.ML	Fri Jan 02 00:21:59 2009 +0100
@@ -1,9 +1,5 @@
-(*  Title:      HOL/ROOT.ML
- 
-Classical Higher-order Logic -- batteries included.
-*)
+(* Classical Higher-order Logic -- batteries included *)
 
 use_thy "Complex_Main";
 
 val HOL_proofs = ! Proofterm.proofs;
-
diff -r 57f0d287375e -r 5c71a6da989d src/HOL/main.ML
--- a/src/HOL/main.ML	Thu Jan 01 23:31:59 2009 +0100
+++ b/src/HOL/main.ML	Fri Jan 02 00:21:59 2009 +0100
@@ -1,7 +1,2 @@
-(*  Title:      HOL/main.ML
-    ID:         $Id$
- 
-Classical Higher-order Logic -- only "Main".
-*)
-
+(*side-entry for HOL-Main*)
 use_thy "Main";
diff -r 57f0d287375e -r 5c71a6da989d src/HOL/plain.ML
--- a/src/HOL/plain.ML	Thu Jan 01 23:31:59 2009 +0100
+++ b/src/HOL/plain.ML	Fri Jan 02 00:21:59 2009 +0100
@@ -1,6 +1,2 @@
-(*  Title:      HOL/plain.ML
- 
-Classical Higher-order Logic -- plain Tool bootstrap.
-*)
-
+(*side-entry for HOL-Plain*)
 use_thy "Plain";