--- 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
--- 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
--- 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
--- 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;
-
--- 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";
--- 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";