changeset 47047 | 10bece4ac87e |
parent 47045 | 631adf003bb0 |
child 50694 | df8ae0590be2 |
--- a/src/HOL/Tools/Metis/metis_tactic.ML Tue Mar 20 13:53:09 2012 +0100 +++ b/src/HOL/Tools/Metis/metis_tactic.ML Tue Mar 20 13:53:09 2012 +0100 @@ -118,8 +118,8 @@ postfactor = #postfactor Metis_Active.default} val waiting_params = {symbolsWeight = 1.0, - variablesWeight = 0.5, - literalsWeight = 0.1, + variablesWeight = 0.05, + literalsWeight = 0.01, models = []} fun resolution_params ordering = {active = active_params ordering, waiting = waiting_params}