changeset 54556 | dd511ddcb203 |
parent 50530 | 6266e44b3396 |
child 58825 | 2065f49da190 |
54555:e8c5e95d338b | 54556:dd511ddcb203 |
---|---|
6 *) |
6 *) |
7 |
7 |
8 header {* Refute *} |
8 header {* Refute *} |
9 |
9 |
10 theory Refute |
10 theory Refute |
11 imports Hilbert_Choice List Sledgehammer |
11 imports Main |
12 keywords "refute" :: diag and "refute_params" :: thy_decl |
12 keywords "refute" :: diag and "refute_params" :: thy_decl |
13 begin |
13 begin |
14 |
14 |
15 ML_file "refute.ML" |
15 ML_file "refute.ML" |
16 setup Refute.setup |
16 setup Refute.setup |