minimal import
authorhaftmann
Sun May 06 21:49:26 2007 +0200 (2007-05-06)
changeset 22840643bb625a2c3
parent 22839 ede26eb5e549
child 22841 83b9f2d3fb3c
minimal import
src/HOL/Main.thy
     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