src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
changeset 46426 fd15abc50fc1
parent 46415 26153cbe97bf
child 46435 e9c90516bc0d
equal deleted inserted replaced
46425:0a37c1e52c91 46426:fd15abc50fc1
   388           [("verbose", "true"),
   388           [("verbose", "true"),
   389            ("type_enc", type_enc),
   389            ("type_enc", type_enc),
   390            ("strict", strict),
   390            ("strict", strict),
   391            ("lam_trans", lam_trans |> the_default "smart"),
   391            ("lam_trans", lam_trans |> the_default "smart"),
   392            ("uncurried_aliases", uncurried_aliases |> the_default "smart"),
   392            ("uncurried_aliases", uncurried_aliases |> the_default "smart"),
   393            ("preplay_timeout", preplay_timeout),
       
   394            ("max_relevant", max_relevant),
   393            ("max_relevant", max_relevant),
   395            ("slice", slice),
   394            ("slice", slice),
   396            ("timeout", string_of_int timeout),
   395            ("timeout", string_of_int timeout),
   397            ("preplay_timeout", preplay_timeout)]
   396            ("preplay_timeout", preplay_timeout)]
   398     val default_max_relevant =
   397     val default_max_relevant =