author | blanchet |
Wed, 18 Jul 2012 08:44:05 +0200 | |
changeset 49348 | 2250197977dc |
parent 49337 | 8a8d71e34297 |
child 49906 | c0eafbd55de3 |
permissions | -rw-r--r-- |
blanchet@49300 | 1 |
(* Title: HOL/TPTP/MaSh_Eval.thy |
blanchet@49249 | 2 |
Author: Jasmin Blanchette, TU Muenchen |
blanchet@49249 | 3 |
*) |
blanchet@49249 | 4 |
|
blanchet@49300 | 5 |
header {* MaSh Evaluation Driver *} |
blanchet@49249 | 6 |
|
blanchet@49300 | 7 |
theory MaSh_Eval |
blanchet@49348 | 8 |
imports Complex_Main |
blanchet@49300 | 9 |
uses "mash_eval.ML" |
blanchet@49249 | 10 |
begin |
blanchet@49249 | 11 |
|
blanchet@49299 | 12 |
sledgehammer_params |
blanchet@49299 | 13 |
[provers = e, max_relevant = 40, strict, dont_slice, type_enc = poly_guards??, |
blanchet@49299 | 14 |
lam_trans = combs_and_lifting, timeout = 5, dont_preplay, minimize] |
blanchet@49299 | 15 |
|
blanchet@49251 | 16 |
declare [[sledgehammer_instantiate_inducts]] |
blanchet@49251 | 17 |
|
blanchet@49250 | 18 |
ML {* |
blanchet@49300 | 19 |
open MaSh_Eval |
blanchet@49250 | 20 |
*} |
blanchet@49250 | 21 |
|
blanchet@49250 | 22 |
ML {* |
blanchet@49348 | 23 |
val do_it = false (* switch to "true" to generate the files *) |
blanchet@49348 | 24 |
val thy = @{theory Nat} |
blanchet@49266 | 25 |
val params = Sledgehammer_Isar.default_params @{context} [] |
blanchet@49250 | 26 |
*} |
blanchet@49250 | 27 |
|
blanchet@49250 | 28 |
ML {* |
blanchet@49265 | 29 |
if do_it then |
blanchet@49348 | 30 |
evaluate_mash_suggestions @{context} params thy "/tmp/mash_suggestions" |
blanchet@49265 | 31 |
else |
blanchet@49265 | 32 |
() |
blanchet@49250 | 33 |
*} |
blanchet@49250 | 34 |
|
blanchet@49249 | 35 |
end |