author | blanchet |
Wed, 01 Sep 2010 16:11:48 +0200 | |
changeset 38995 | 54b81258c831 |
parent 38994 | 7c655a491bce |
child 38996 | 6905ba37376c |
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML | file | annotate | diff | comparison | revisions |
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Wed Sep 01 11:59:04 2010 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Wed Sep 01 16:11:48 2010 +0200 @@ -19,6 +19,7 @@ ("elim_bonus", SF.elim_bonus), ("simp_bonus", SF.simp_bonus), ("local_bonus", SF.local_bonus), + ("assum_bonus", SF.assum_bonus), ("chained_bonus", SF.chained_bonus), ("max_imperfect", SF.max_imperfect), ("max_imperfect_exp", SF.max_imperfect_exp),