| changeset 40178 | 00152d17855b |
| parent 40121 | e7a80c6752c9 |
| child 46950 | d0181abdbdac |
| 40166:d3bc972b7d9d | 40178:00152d17855b |
|---|---|
6 *) |
6 *) |
7 |
7 |
8 header {* Refute *} |
8 header {* Refute *} |
9 |
9 |
10 theory Refute |
10 theory Refute |
11 imports Hilbert_Choice List |
11 imports Hilbert_Choice List Sledgehammer |
12 uses "Tools/refute.ML" |
12 uses "Tools/refute.ML" |
13 begin |
13 begin |
14 |
14 |
15 setup Refute.setup |
15 setup Refute.setup |
16 |
16 |