src/HOL/Main.thy
changeset 22840 643bb625a2c3
parent 21254 d53f76357f41
child 23165 5d319b0f8bf9
     1.1 --- a/src/HOL/Main.thy	Sun May 06 21:49:24 2007 +0200
     1.2 +++ b/src/HOL/Main.thy	Sun May 06 21:49:26 2007 +0200
     1.3 @@ -5,17 +5,17 @@
     1.4  header {* Main HOL *}
     1.5  
     1.6  theory Main
     1.7 -imports SAT ATP_Linkup
     1.8 +imports Map Hilbert_Choice ATP_Linkup
     1.9  begin
    1.10  
    1.11  text {*
    1.12    Theory @{text Main} includes everything.  Note that theory @{text
    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  *}
    1.18  
    1.19 -text {* \medskip Late clause setup: installs \emph{all} known theorems
    1.20 -  into the clause cache; cf.\ theory @{text ATP_Linkup}. *}
    1.21 -
    1.22  setup ResAxioms.setup
    1.23  
    1.24  end