equal
deleted
inserted
replaced
229 if Config.get ctxt config_fast_solver |
229 if Config.get ctxt config_fast_solver |
230 then assume_tac ctxt ORELSE' (eresolve_tac ctxt [notE]) |
230 then assume_tac ctxt ORELSE' (eresolve_tac ctxt [notE]) |
231 else K no_tac); |
231 else K no_tac); |
232 \<close> |
232 \<close> |
233 |
233 |
234 setup \<open>map_theory_simpset (fn ctxt => ctxt addSSolver fast_solver)\<close> |
234 setup \<open>map_theory_simpset (fn ctxt => ctxt |> Simplifier.add_safe_solver fast_solver)\<close> |
235 |
235 |
236 ML \<open>val temp_elim = make_elim oo temp_use\<close> |
236 ML \<open>val temp_elim = make_elim oo temp_use\<close> |
237 |
237 |
238 |
238 |
239 |
239 |