equal
deleted
inserted
replaced
225 *) |
225 *) |
226 ML {* |
226 ML {* |
227 val config_fast_solver = Attrib.setup_config_bool @{binding fast_solver} (K false); |
227 val config_fast_solver = Attrib.setup_config_bool @{binding fast_solver} (K false); |
228 val fast_solver = mk_solver "fast_solver" (fn ctxt => |
228 val fast_solver = mk_solver "fast_solver" (fn ctxt => |
229 if Config.get ctxt config_fast_solver |
229 if Config.get ctxt config_fast_solver |
230 then assume_tac ORELSE' (etac notE) |
230 then assume_tac ctxt ORELSE' (etac notE) |
231 else K no_tac); |
231 else K no_tac); |
232 *} |
232 *} |
233 |
233 |
234 setup {* map_theory_simpset (fn ctxt => ctxt addSSolver fast_solver) *} |
234 setup {* map_theory_simpset (fn ctxt => ctxt addSSolver fast_solver) *} |
235 |
235 |