| changeset 16417 | 9bc16273c2d4 |
| parent 15293 | 7797a04cc188 |
| child 16870 | a1155e140597 |
| 16416:6061ae1f90f2 | 16417:9bc16273c2d4 |
|---|---|
8 |
8 |
9 header {* Refute *} |
9 header {* Refute *} |
10 |
10 |
11 theory Refute |
11 theory Refute |
12 imports Map |
12 imports Map |
13 files "Tools/prop_logic.ML" |
13 uses "Tools/prop_logic.ML" |
14 "Tools/sat_solver.ML" |
14 "Tools/sat_solver.ML" |
15 "Tools/refute.ML" |
15 "Tools/refute.ML" |
16 "Tools/refute_isar.ML" |
16 "Tools/refute_isar.ML" |
17 begin |
17 begin |
18 |
18 |