src/HOL/Main.thy
changeset 24632 779fc4fcbf8b
parent 23165 5d319b0f8bf9
child 24644 66ef82187de1
     1.1 --- a/src/HOL/Main.thy	Tue Sep 18 16:08:08 2007 +0200
     1.2 +++ b/src/HOL/Main.thy	Tue Sep 18 17:53:37 2007 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* Main HOL *}
     1.5  
     1.6  theory Main
     1.7 -imports Map Hilbert_Choice ATP_Linkup
     1.8 +imports Map 
     1.9  begin
    1.10  
    1.11  text {*
    1.12 @@ -13,10 +13,11 @@
    1.13    PreList} already includes most HOL theories.
    1.14  
    1.15    \medskip Late clause setup: installs \emph{all} known theorems
    1.16 -  into the clause cache; cf.\ theory @{text ATP_Linkup}.
    1.17 +  into the clause cache; cf.\ theory @{text ATP_Linkup}. 
    1.18 +  FIXME: delete once end_theory actions are installed!
    1.19  *}
    1.20  
    1.21 -setup ResAxioms.setup
    1.22 +setup ResAxioms.clause_cache_setup
    1.23  
    1.24  ML {* val HOL_proofs = !proofs *}
    1.25