| author | wenzelm |
| Wed, 01 Aug 2007 16:55:39 +0200 | |
| changeset 24111 | 20e74aa5f56b |
| parent 23165 | 5d319b0f8bf9 |
| child 24632 | 779fc4fcbf8b |
| permissions | -rw-r--r-- |
| 17602 | 1 |
(* Title: HOL/Main.thy |
2 |
ID: $Id$ |
|
3 |
*) |
|
| 9619 | 4 |
|
| 12024 | 5 |
header {* Main HOL *}
|
6 |
||
| 15131 | 7 |
theory Main |
| 22840 | 8 |
imports Map Hilbert_Choice ATP_Linkup |
| 15131 | 9 |
begin |
|
9650
6f0b89f2a1f9
Main now new-style theory; added Main.ML for compatibility;
wenzelm
parents:
9619
diff
changeset
|
10 |
|
| 12024 | 11 |
text {*
|
12 |
Theory @{text Main} includes everything. Note that theory @{text
|
|
13 |
PreList} already includes most HOL theories. |
|
| 22840 | 14 |
|
15 |
\medskip Late clause setup: installs \emph{all} known theorems
|
|
16 |
into the clause cache; cf.\ theory @{text ATP_Linkup}.
|
|
| 19608 | 17 |
*} |
|
17395
a05e20f6a31a
hide the rather generic names used in theory Commutative_Ring;
wenzelm
parents:
17386
diff
changeset
|
18 |
|
|
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18315
diff
changeset
|
19 |
setup ResAxioms.setup |
| 14350 | 20 |
|
| 23165 | 21 |
ML {* val HOL_proofs = !proofs *}
|
22 |
||
|
9650
6f0b89f2a1f9
Main now new-style theory; added Main.ML for compatibility;
wenzelm
parents:
9619
diff
changeset
|
23 |
end |