equal
deleted
inserted
replaced
359 val Ord_atomize = |
359 val Ord_atomize = |
360 atomize ([(@{const_name oall}, @{thms ospec}), (@{const_name rall}, @{thms rspec})] @ |
360 atomize ([(@{const_name oall}, @{thms ospec}), (@{const_name rall}, @{thms rspec})] @ |
361 ZF_conn_pairs, ZF_mem_pairs); |
361 ZF_conn_pairs, ZF_mem_pairs); |
362 *} |
362 *} |
363 declaration {* fn _ => |
363 declaration {* fn _ => |
364 Simplifier.map_ss (Simplifier.set_mksimps (K (map mk_eq o Ord_atomize o gen_all))) |
364 Simplifier.map_ss (Simplifier.set_mksimps (fn ctxt => |
|
365 map mk_eq o Ord_atomize o Drule.gen_all (Variable.maxidx_of ctxt))) |
365 *} |
366 *} |
366 |
367 |
367 text {* Setting up the one-point-rule simproc *} |
368 text {* Setting up the one-point-rule simproc *} |
368 |
369 |
369 simproc_setup defined_rex ("\<exists>x[M]. P(x) & Q(x)") = {* |
370 simproc_setup defined_rex ("\<exists>x[M]. P(x) & Q(x)") = {* |