--- a/src/HOL/Main.thy Thu Sep 27 17:28:05 2007 +0200
+++ b/src/HOL/Main.thy Thu Sep 27 17:55:28 2007 +0200
@@ -11,14 +11,8 @@
text {*
Theory @{text Main} includes everything. Note that theory @{text
PreList} already includes most HOL theories.
-
- \medskip Late clause setup: installs \emph{all} known theorems
- into the clause cache; cf.\ theory @{text ATP_Linkup}.
- FIXME: delete once @{text end_theory} actions are installed!
*}
-setup ResAxioms.clause_cache_setup
-
ML {* val HOL_proofs = !proofs *}
end