equal
deleted
inserted
replaced
539 #> Parse.xthm #> fst |
539 #> Parse.xthm #> fst |
540 val thms = named_thms |> maps snd |
540 val thms = named_thms |> maps snd |
541 val facts = named_thms |> map (ref_of_str o fst o fst) |
541 val facts = named_thms |> map (ref_of_str o fst o fst) |
542 val fact_override = {add = facts, del = [], only = true} |
542 val fact_override = {add = facts, del = [], only = true} |
543 fun my_timeout time_slice = |
543 fun my_timeout time_slice = |
544 timeout |> Time.toReal |> curry Real.* time_slice |> Time.fromReal |
544 timeout |> Time.toReal |> curry (op *) time_slice |> Time.fromReal |
545 fun sledge_tac time_slice prover type_enc = |
545 fun sledge_tac time_slice prover type_enc = |
546 Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt |
546 Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt |
547 (override_params prover type_enc (my_timeout time_slice)) fact_override [] |
547 (override_params prover type_enc (my_timeout time_slice)) fact_override [] |
548 in |
548 in |
549 if !meth = "sledgehammer_tac" then |
549 if !meth = "sledgehammer_tac" then |