| author | paulson |
| Fri, 25 Aug 2006 18:44:59 +0200 | |
| changeset 20414 | 029c4f9dc6f4 |
| parent 20362 | bbff23c3e2ca |
| child 21254 | d53f76357f41 |
| 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 |
|
17905
1574533861b1
Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
mengj
parents:
17721
diff
changeset
|
8 |
imports SAT Reconstruction ResAtpMethods |
| 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. |
|
| 19608 | 14 |
*} |
|
17395
a05e20f6a31a
hide the rather generic names used in theory Commutative_Ring;
wenzelm
parents:
17386
diff
changeset
|
15 |
|
|
20414
029c4f9dc6f4
replaced skolem declarations by automatic skolemization of everything
paulson
parents:
20362
diff
changeset
|
16 |
text {* \medskip Late clause setup: installs \emph{all} known theorems
|
|
029c4f9dc6f4
replaced skolem declarations by automatic skolemization of everything
paulson
parents:
20362
diff
changeset
|
17 |
into the clause cache; cf.\ theory @{text Reconstruction}. *}
|
| 14350 | 18 |
|
|
18510
0a6c24f549c3
the "skolem" attribute and better initialization of the clause database
paulson
parents:
18315
diff
changeset
|
19 |
setup ResAxioms.setup |
| 14350 | 20 |
|
|
9650
6f0b89f2a1f9
Main now new-style theory; added Main.ML for compatibility;
wenzelm
parents:
9619
diff
changeset
|
21 |
end |