equal
deleted
inserted
replaced
327 (*We use a MINIMAL simpset. Even FOL_ss contains too many simpules. |
327 (*We use a MINIMAL simpset. Even FOL_ss contains too many simpules. |
328 If the premises get simplified, then the proofs could fail.*) |
328 If the premises get simplified, then the proofs could fail.*) |
329 val min_ss = Simplifier.global_context thy empty_ss |
329 val min_ss = Simplifier.global_context thy empty_ss |
330 setmksimps (K (map mk_eq o ZF_atomize o gen_all)) |
330 setmksimps (K (map mk_eq o ZF_atomize o gen_all)) |
331 setSolver (mk_solver "minimal" |
331 setSolver (mk_solver "minimal" |
332 (fn prems => resolve_tac (triv_rls@prems) |
332 (fn ss => resolve_tac (triv_rls @ prems_of_ss ss) |
333 ORELSE' assume_tac |
333 ORELSE' assume_tac |
334 ORELSE' etac @{thm FalseE})); |
334 ORELSE' etac @{thm FalseE})); |
335 |
335 |
336 val quant_induct = |
336 val quant_induct = |
337 Goal.prove_global thy1 [] ind_prems |
337 Goal.prove_global thy1 [] ind_prems |