src/ZF/pair.thy
changeset 42794 07155da3b2f4
parent 42459 38b9f023cc34
child 42795 66fcc9882784
     1.1 --- a/src/ZF/pair.thy	Fri May 13 22:55:00 2011 +0200
     1.2 +++ b/src/ZF/pair.thy	Fri May 13 23:24:06 2011 +0200
     1.3 @@ -1,7 +1,6 @@
     1.4  (*  Title:      ZF/pair.thy
     1.5      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.6      Copyright   1992  University of Cambridge
     1.7 -
     1.8  *)
     1.9  
    1.10  header{*Ordered Pairs*}
    1.11 @@ -10,6 +9,14 @@
    1.12  uses "simpdata.ML"
    1.13  begin
    1.14  
    1.15 +declaration {*
    1.16 +  fn _ => Simplifier.map_ss (fn ss =>
    1.17 +    ss setmksimps (K (map mk_eq o ZF_atomize o gen_all))
    1.18 +    addcongs [@{thm if_weak_cong}])
    1.19 +*}
    1.20 +
    1.21 +ML {* val ZF_ss = @{simpset} *}
    1.22 +
    1.23  simproc_setup defined_Bex ("EX x:A. P(x) & Q(x)") = {*
    1.24    let
    1.25      val unfold_bex_tac = unfold_tac @{thms Bex_def};