src/HOL/Main.thy
changeset 24742 73b8b42a36b6
parent 24699 c6674504103f
child 25223 7463251e7273
     1.1 --- a/src/HOL/Main.thy	Thu Sep 27 17:28:05 2007 +0200
     1.2 +++ b/src/HOL/Main.thy	Thu Sep 27 17:55:28 2007 +0200
     1.3 @@ -11,14 +11,8 @@
     1.4  text {*
     1.5    Theory @{text Main} includes everything.  Note that theory @{text
     1.6    PreList} already includes most HOL theories.
     1.7 -
     1.8 -  \medskip Late clause setup: installs \emph{all} known theorems
     1.9 -  into the clause cache; cf.\ theory @{text ATP_Linkup}. 
    1.10 -  FIXME: delete once @{text end_theory} actions are installed!
    1.11  *}
    1.12  
    1.13 -setup ResAxioms.clause_cache_setup
    1.14 -
    1.15  ML {* val HOL_proofs = !proofs *}
    1.16  
    1.17  end