tuned header and description of boot files;
authorwenzelm
Fri Jan 02 00:21:59 2009 +0100 (2009-01-02)
changeset 293045c71a6da989d
parent 29303 57f0d287375e
child 29305 76af2a3c9d28
child 29334 3eb95594ba89
tuned header and description of boot files;
src/HOL/Complex_Main.thy
src/HOL/Main.thy
src/HOL/Plain.thy
src/HOL/ROOT.ML
src/HOL/main.ML
src/HOL/plain.ML
     1.1 --- a/src/HOL/Complex_Main.thy	Thu Jan 01 23:31:59 2009 +0100
     1.2 +++ b/src/HOL/Complex_Main.thy	Fri Jan 02 00:21:59 2009 +0100
     1.3 @@ -1,9 +1,4 @@
     1.4 -(*  Title:      HOL/Complex_Main.thy
     1.5 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.6 -    Copyright   2003  University of Cambridge
     1.7 -*)
     1.8 -
     1.9 -header{*Comprehensive Complex Theory*}
    1.10 +header {* Comprehensive Complex Theory *}
    1.11  
    1.12  theory Complex_Main
    1.13  imports
     2.1 --- a/src/HOL/Main.thy	Thu Jan 01 23:31:59 2009 +0100
     2.2 +++ b/src/HOL/Main.thy	Fri Jan 02 00:21:59 2009 +0100
     2.3 @@ -1,13 +1,14 @@
     2.4 -(*  Title:      HOL/Main.thy
     2.5 -    ID:         $Id$
     2.6 -*)
     2.7 -
     2.8  header {* Main HOL *}
     2.9  
    2.10  theory Main
    2.11  imports Plain Code_Eval Map Nat_Int_Bij Recdef
    2.12  begin
    2.13  
    2.14 +text {*
    2.15 +  Classical Higher-order Logic -- only ``Main'', excluding real and
    2.16 +  complex numbers etc.
    2.17 +*}
    2.18 +
    2.19  text {* See further \cite{Nipkow-et-al:2002:tutorial} *}
    2.20  
    2.21  end
     3.1 --- a/src/HOL/Plain.thy	Thu Jan 01 23:31:59 2009 +0100
     3.2 +++ b/src/HOL/Plain.thy	Fri Jan 02 00:21:59 2009 +0100
     3.3 @@ -1,15 +1,14 @@
     3.4 -(*  Title:      HOL/Plain.thy
     3.5 -    ID:         $Id$
     3.6 -
     3.7 -Contains fundamental HOL tools and packages.  Does not include Hilbert_Choice.
     3.8 -*)
     3.9 -
    3.10  header {* Plain HOL *}
    3.11  
    3.12  theory Plain
    3.13  imports Datatype FunDef Record SAT Extraction
    3.14  begin
    3.15  
    3.16 +text {*
    3.17 +  Plain bootstrap of fundamental HOL tools and packages; does not
    3.18 +  include @{text Hilbert_Choice}.
    3.19 +*}
    3.20 +
    3.21  ML {* path_add "~~/src/HOL/Library" *}
    3.22  
    3.23  end
     4.1 --- a/src/HOL/ROOT.ML	Thu Jan 01 23:31:59 2009 +0100
     4.2 +++ b/src/HOL/ROOT.ML	Fri Jan 02 00:21:59 2009 +0100
     4.3 @@ -1,9 +1,5 @@
     4.4 -(*  Title:      HOL/ROOT.ML
     4.5 - 
     4.6 -Classical Higher-order Logic -- batteries included.
     4.7 -*)
     4.8 +(* Classical Higher-order Logic -- batteries included *)
     4.9  
    4.10  use_thy "Complex_Main";
    4.11  
    4.12  val HOL_proofs = ! Proofterm.proofs;
    4.13 -
     5.1 --- a/src/HOL/main.ML	Thu Jan 01 23:31:59 2009 +0100
     5.2 +++ b/src/HOL/main.ML	Fri Jan 02 00:21:59 2009 +0100
     5.3 @@ -1,7 +1,2 @@
     5.4 -(*  Title:      HOL/main.ML
     5.5 -    ID:         $Id$
     5.6 - 
     5.7 -Classical Higher-order Logic -- only "Main".
     5.8 -*)
     5.9 -
    5.10 +(*side-entry for HOL-Main*)
    5.11  use_thy "Main";
     6.1 --- a/src/HOL/plain.ML	Thu Jan 01 23:31:59 2009 +0100
     6.2 +++ b/src/HOL/plain.ML	Fri Jan 02 00:21:59 2009 +0100
     6.3 @@ -1,6 +1,2 @@
     6.4 -(*  Title:      HOL/plain.ML
     6.5 - 
     6.6 -Classical Higher-order Logic -- plain Tool bootstrap.
     6.7 -*)
     6.8 -
     6.9 +(*side-entry for HOL-Plain*)
    6.10  use_thy "Plain";