src/HOL/Main.thy
changeset 21254 d53f76357f41
parent 20414 029c4f9dc6f4
child 22840 643bb625a2c3
     1.1 --- a/src/HOL/Main.thy	Wed Nov 08 21:45:14 2006 +0100
     1.2 +++ b/src/HOL/Main.thy	Wed Nov 08 21:45:15 2006 +0100
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* Main HOL *}
     1.5  
     1.6  theory Main
     1.7 -imports SAT Reconstruction ResAtpMethods
     1.8 +imports SAT ATP_Linkup
     1.9  begin
    1.10  
    1.11  text {*
    1.12 @@ -14,7 +14,7 @@
    1.13  *}
    1.14  
    1.15  text {* \medskip Late clause setup: installs \emph{all} known theorems
    1.16 -  into the clause cache; cf.\ theory @{text Reconstruction}. *}
    1.17 +  into the clause cache; cf.\ theory @{text ATP_Linkup}. *}
    1.18  
    1.19  setup ResAxioms.setup
    1.20