equal
deleted
inserted
replaced
686 () |
686 () |
687 val fact_filter = |
687 val fact_filter = |
688 case fact_filter of |
688 case fact_filter of |
689 SOME ff => (() |> ff <> mepoN ? maybe_learn; ff) |
689 SOME ff => (() |> ff <> mepoN ? maybe_learn; ff) |
690 | NONE => |
690 | NONE => |
691 if mash_can_suggest_facts ctxt then (maybe_learn (); meshN) |
691 if is_smt_prover ctxt prover then mepoN |
|
692 else if mash_can_suggest_facts ctxt then (maybe_learn (); meshN) |
692 else if mash_could_suggest_facts () then (maybe_learn (); mepoN) |
693 else if mash_could_suggest_facts () then (maybe_learn (); mepoN) |
693 else mepoN |
694 else mepoN |
694 val add_ths = Attrib.eval_thms ctxt add |
695 val add_ths = Attrib.eval_thms ctxt add |
695 fun prepend_facts ths accepts = |
696 fun prepend_facts ths accepts = |
696 ((facts |> filter (member Thm.eq_thm_prop ths o snd)) @ |
697 ((facts |> filter (member Thm.eq_thm_prop ths o snd)) @ |