equal
deleted
inserted
replaced
325 |
325 |
326 (*We use a MINIMAL simpset. Even FOL_ss contains too many simpules. |
326 (*We use a MINIMAL simpset. Even FOL_ss contains too many simpules. |
327 If the premises get simplified, then the proofs could fail.*) |
327 If the premises get simplified, then the proofs could fail.*) |
328 val min_ss = |
328 val min_ss = |
329 (empty_simpset (Proof_Context.init_global thy) |
329 (empty_simpset (Proof_Context.init_global thy) |
330 |> Simplifier.set_mksimps (K (map mk_eq o ZF_atomize o gen_all))) |
330 |> Simplifier.set_mksimps (fn ctxt => |
|
331 map mk_eq o ZF_atomize o Drule.gen_all (Variable.maxidx_of ctxt))) |
331 setSolver (mk_solver "minimal" |
332 setSolver (mk_solver "minimal" |
332 (fn ctxt => resolve_tac ctxt (triv_rls @ Simplifier.prems_of ctxt) |
333 (fn ctxt => resolve_tac ctxt (triv_rls @ Simplifier.prems_of ctxt) |
333 ORELSE' assume_tac ctxt |
334 ORELSE' assume_tac ctxt |
334 ORELSE' eresolve_tac ctxt @{thms FalseE})); |
335 ORELSE' eresolve_tac ctxt @{thms FalseE})); |
335 |
336 |