tuned imports
authorhaftmann
Wed Apr 02 15:58:57 2008 +0200 (2008-04-02)
changeset 26521f8c4e79db153
parent 26520 9e7b7c478cb1
child 26522 b05cdd060c3e
tuned imports
src/HOL/Refute.thy
src/HOL/SAT.thy
     1.1 --- a/src/HOL/Refute.thy	Wed Apr 02 15:58:43 2008 +0200
     1.2 +++ b/src/HOL/Refute.thy	Wed Apr 02 15:58:57 2008 +0200
     1.3 @@ -9,11 +9,12 @@
     1.4  header {* Refute *}
     1.5  
     1.6  theory Refute
     1.7 -imports Datatype
     1.8 -uses "Tools/prop_logic.ML"
     1.9 -     "Tools/sat_solver.ML"
    1.10 -     "Tools/refute.ML"
    1.11 -     "Tools/refute_isar.ML"
    1.12 +imports Inductive
    1.13 +uses
    1.14 +  "Tools/prop_logic.ML"
    1.15 +  "Tools/sat_solver.ML"
    1.16 +  "Tools/refute.ML"
    1.17 +  "Tools/refute_isar.ML"
    1.18  begin
    1.19  
    1.20  setup Refute.setup
     2.1 --- a/src/HOL/SAT.thy	Wed Apr 02 15:58:43 2008 +0200
     2.2 +++ b/src/HOL/SAT.thy	Wed Apr 02 15:58:57 2008 +0200
     2.3 @@ -8,12 +8,11 @@
     2.4  
     2.5  header {* Reconstructing external resolution proofs for propositional logic *}
     2.6  
     2.7 -theory SAT imports Refute
     2.8 -
     2.9 +theory SAT
    2.10 +imports Refute
    2.11  uses
    2.12 -     "Tools/cnf_funcs.ML"
    2.13 -     "Tools/sat_funcs.ML"
    2.14 -
    2.15 +  "Tools/cnf_funcs.ML"
    2.16 +  "Tools/sat_funcs.ML"
    2.17  begin
    2.18  
    2.19  text {* \medskip Late package setup: default values for refute, see
    2.20 @@ -27,7 +26,6 @@
    2.21    maxtime=60,
    2.22    satsolver="auto"]
    2.23  
    2.24 -
    2.25  ML {* structure sat = SATFunc(structure cnf = cnf); *}
    2.26  
    2.27  method_setup sat = {* Method.no_args (Method.SIMPLE_METHOD' sat.sat_tac) *}