src/HOL/Refute.thy
changeset 34018 39f21f7bad7e
parent 33593 ef54e2108b74
child 34120 f9920a3ddf50
equal deleted inserted replaced
34017:ef2776c89799 34018:39f21f7bad7e
     8 header {* Refute *}
     8 header {* Refute *}
     9 
     9 
    10 theory Refute
    10 theory Refute
    11 imports Hilbert_Choice List
    11 imports Hilbert_Choice List
    12 uses
    12 uses
    13   "Tools/prop_logic.ML"
       
    14   "Tools/sat_solver.ML"
       
    15   "Tools/refute.ML"
    13   "Tools/refute.ML"
    16   "Tools/refute_isar.ML"
    14   "Tools/refute_isar.ML"
    17 begin
    15 begin
    18 
    16 
    19 setup Refute.setup
    17 setup Refute.setup