changeset 34018 | 39f21f7bad7e |
parent 33593 | ef54e2108b74 |
child 34120 | f9920a3ddf50 |
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 |