equal
deleted
inserted
replaced
12 Theory @{text Main} includes everything. Note that theory @{text |
12 Theory @{text Main} includes everything. Note that theory @{text |
13 PreList} already includes most HOL theories. |
13 PreList} already includes most HOL theories. |
14 |
14 |
15 \medskip Late clause setup: installs \emph{all} known theorems |
15 \medskip Late clause setup: installs \emph{all} known theorems |
16 into the clause cache; cf.\ theory @{text ATP_Linkup}. |
16 into the clause cache; cf.\ theory @{text ATP_Linkup}. |
17 FIXME: delete once end_theory actions are installed! |
17 FIXME: delete once @{text end_theory} actions are installed! |
18 *} |
18 *} |
19 |
19 |
20 setup ResAxioms.clause_cache_setup |
20 setup ResAxioms.clause_cache_setup |
21 |
21 |
22 ML {* val HOL_proofs = !proofs *} |
22 ML {* val HOL_proofs = !proofs *} |