# HG changeset patch # User blanchet # Date 1401455741 -7200 # Node ID 4ddf5a8f8f3861afbb1e913bddcb86f523a03456 # Parent 8402ac8c826f71bcf0481dcfe18a071108259ba2 make SML code closer to Python code when 'nb_kuehlwein_style' is true diff -r 8402ac8c826f -r 4ddf5a8f8f38 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri May 30 15:15:02 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri May 30 15:15:41 2014 +0200 @@ -460,7 +460,7 @@ ret [] (Integer.max 0 (num_visible_facts - max_suggs)) end -val nb_def_prior_weight = 20 (* FUDGE *) +val nb_def_prior_weight = 21 (* FUDGE *) (* TODO: Either use IDF or don't use it. See commented out code portions below. *) @@ -497,7 +497,7 @@ val nb_kuehlwein_style = false val nb_tau = if nb_kuehlwein_style then 0.05 else 0.02 (* FUDGE *) -val nb_pos_weight = if nb_kuehlwein_style then 20.0 else 2.0 (* FUDGE *) +val nb_pos_weight = if nb_kuehlwein_style then 10.0 else 2.0 (* FUDGE *) val nb_def_val = ~15.0 (* FUDGE *) fun naive_bayes_query _ (* num_facts *) num_visible_facts max_suggs feats (tfreq, sfreq (*, dffreq*)) =