author wenzelm Fri Jan 02 00:21:59 2009 +0100 (2009-01-02) changeset 29304 5c71a6da989d parent 29303 57f0d287375e child 29305 76af2a3c9d28 child 29334 3eb95594ba89
tuned header and description of boot files;
 src/HOL/Complex_Main.thy file | annotate | diff | revisions src/HOL/Main.thy file | annotate | diff | revisions src/HOL/Plain.thy file | annotate | diff | revisions src/HOL/ROOT.ML file | annotate | diff | revisions src/HOL/main.ML file | annotate | diff | revisions src/HOL/plain.ML file | annotate | diff | revisions
```     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.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";
```