src/ZF/OrdQuant.thy
changeset 26339 7825c83c9eff
parent 24893 b8ef7afe3a6b
child 26480 544cef16045b
equal deleted inserted replaced
26338:f8ed02f22433 26339:7825c83c9eff
   360 {*
   360 {*
   361 val Ord_atomize =
   361 val Ord_atomize =
   362     atomize ([("OrdQuant.oall", [@{thm ospec}]),("OrdQuant.rall", [@{thm rspec}])]@
   362     atomize ([("OrdQuant.oall", [@{thm ospec}]),("OrdQuant.rall", [@{thm rspec}])]@
   363                  ZF_conn_pairs,
   363                  ZF_conn_pairs,
   364              ZF_mem_pairs);
   364              ZF_mem_pairs);
   365 change_simpset (fn ss => ss setmksimps (map mk_eq o Ord_atomize o gen_all));
   365 *}
       
   366 declaration {* fn _ =>
       
   367   Simplifier.map_ss (fn ss => ss setmksimps (map mk_eq o Ord_atomize o gen_all))
   366 *}
   368 *}
   367 
   369 
   368 text {* Setting up the one-point-rule simproc *}
   370 text {* Setting up the one-point-rule simproc *}
   369 
   371 
   370 ML_setup {*
   372 ML_setup {*