equal
deleted
inserted
replaced
8 header {* Refute *} |
8 header {* Refute *} |
9 |
9 |
10 theory Refute |
10 theory Refute |
11 imports Hilbert_Choice List Sledgehammer |
11 imports Hilbert_Choice List Sledgehammer |
12 keywords "refute" :: diag and "refute_params" :: thy_decl |
12 keywords "refute" :: diag and "refute_params" :: thy_decl |
13 uses "Tools/refute.ML" |
|
14 begin |
13 begin |
15 |
14 |
|
15 ML_file "Tools/refute.ML" |
16 setup Refute.setup |
16 setup Refute.setup |
17 |
17 |
18 refute_params |
18 refute_params |
19 [itself = 1, |
19 [itself = 1, |
20 minsize = 1, |
20 minsize = 1, |