author | berghofe |
Wed, 19 Sep 2007 12:17:13 +0200 | |
changeset 24644 | 66ef82187de1 |
parent 24632 | 779fc4fcbf8b |
child 24699 | c6674504103f |
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 |
24632 | 8 |
imports Map |
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 |
|
24632 | 16 |
into the clause cache; cf.\ theory @{text ATP_Linkup}. |
24644
66ef82187de1
Enclosed end_theory in text antiquotation to make LaTeX happy.
berghofe
parents:
24632
diff
changeset
|
17 |
FIXME: delete once @{text end_theory} actions are installed! |
19608 | 18 |
*} |
17395
a05e20f6a31a
hide the rather generic names used in theory Commutative_Ring;
wenzelm
parents:
17386
diff
changeset
|
19 |
|
24632 | 20 |
setup ResAxioms.clause_cache_setup |
14350 | 21 |
|
23165 | 22 |
ML {* val HOL_proofs = !proofs *} |
23 |
||
9650
6f0b89f2a1f9
Main now new-style theory; added Main.ML for compatibility;
wenzelm
parents:
9619
diff
changeset
|
24 |
end |