| changeset 15140 | 322485b816ac |
| parent 15131 | c69542757a4d |
| child 15293 | 7797a04cc188 |
| 15139:58cd3404cf75 | 15140:322485b816ac |
|---|---|
7 *) |
7 *) |
8 |
8 |
9 header {* Refute *} |
9 header {* Refute *} |
10 |
10 |
11 theory Refute |
11 theory Refute |
12 import Map |
12 imports Map |
13 files "Tools/prop_logic.ML" |
13 files "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 |