author | blanchet |
Thu, 17 Oct 2013 01:34:34 +0200 | |
changeset 54129 | 9ee9eee93c06 |
parent 54128 | da2b75a04da6 |
child 54130 | b4e6cd4cab92 |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Oct 17 01:22:15 2013 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Oct 17 01:34:34 2013 +0200 @@ -388,6 +388,7 @@ else (); mash_learn ctxt + (* TODO: Use MaSh mode instead and have the special defaults hardcoded in "get_params" *) (get_params Normal ctxt ([("timeout", [string_of_real default_learn_prover_timeout]),