# HG changeset patch
# User blanchet
# Date 1403250931 -7200
# Node ID bb671e6b740dcd4b74e24593202079c609a165f2
# Parent  6907432c47b9cd79315f75091411d0f4ecaef3a5
changed default MaSh parameters based on (in vitro) evaluation

diff -r 6907432c47b9 -r bb671e6b740d src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jun 20 09:42:36 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jun 20 09:55:31 2014 +0200
@@ -160,7 +160,7 @@
 | MaSh_SML_NB of bool * bool
 | MaSh_SML_NB_Py
 
-val default_MaSh_SML_NB = MaSh_SML_NB (false, false)
+val default_MaSh_SML_NB = MaSh_SML_NB (false, true)
 
 fun mash_engine () =
   let val flag1 = Options.default_string @{system_option MaSh} in