src/HOL/Tools/Metis/metis_tactic.ML
changeset 47047 10bece4ac87e
parent 47045 631adf003bb0
child 50694 df8ae0590be2
equal deleted inserted replaced
47046:62ca06cc5a99 47047:10bece4ac87e
   116   {clause = clause_params ordering,
   116   {clause = clause_params ordering,
   117    prefactor = #prefactor Metis_Active.default,
   117    prefactor = #prefactor Metis_Active.default,
   118    postfactor = #postfactor Metis_Active.default}
   118    postfactor = #postfactor Metis_Active.default}
   119 val waiting_params =
   119 val waiting_params =
   120   {symbolsWeight = 1.0,
   120   {symbolsWeight = 1.0,
   121    variablesWeight = 0.5,
   121    variablesWeight = 0.05,
   122    literalsWeight = 0.1,
   122    literalsWeight = 0.01,
   123    models = []}
   123    models = []}
   124 fun resolution_params ordering =
   124 fun resolution_params ordering =
   125   {active = active_params ordering, waiting = waiting_params}
   125   {active = active_params ordering, waiting = waiting_params}
   126 
   126 
   127 fun kbo_advisory_simp_ordering ord_info =
   127 fun kbo_advisory_simp_ordering ord_info =