| changeset 57133 | afa80e25a5f3 |
| parent 57132 | 4ddf5a8f8f38 |
| child 57150 | f591096a9c94 |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri May 30 15:15:41 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri May 30 16:00:54 2014 +0200 @@ -523,7 +523,7 @@ val fold_sfh = if nb_kuehlwein_style then - (fn (f, sf) => fn sow => sow - tfidf f * (tfreq / Math.ln (Real.fromInt sf))) + (fn (f, sf) => fn sow => sow - tfidf f * Math.ln (Real.fromInt sf / tfreq)) else (fn (f, sf) => fn sow => sow + tfidf f * Math.ln (1.0 + (1.0 - Real.fromInt sf) / tfreq))