equal
deleted
inserted
replaced
31 ML_file "Tools/Sledgehammer/sledgehammer_mepo.ML" |
31 ML_file "Tools/Sledgehammer/sledgehammer_mepo.ML" |
32 ML_file "Tools/Sledgehammer/sledgehammer_mash.ML" |
32 ML_file "Tools/Sledgehammer/sledgehammer_mash.ML" |
33 ML_file "Tools/Sledgehammer/sledgehammer.ML" |
33 ML_file "Tools/Sledgehammer/sledgehammer.ML" |
34 ML_file "Tools/Sledgehammer/sledgehammer_commands.ML" |
34 ML_file "Tools/Sledgehammer/sledgehammer_commands.ML" |
35 |
35 |
|
36 method_setup skolem = {* |
|
37 Scan.succeed (SIMPLE_METHOD' o Sledgehammer_Proof_Methods.skolem_tac) |
|
38 *} "solve skolemization goals" |
|
39 |
36 end |
40 end |