src/ZF/Pair.ML

  (fn _=> [ (resolve_tac [extension RS iff_trans] 1),
            (fast_tac upair_cs 1) ]);
 
 val Pair_iff = prove_goalw ZF.thy [Pair_def]
     "<a,b> = <c,d> <-> a=c & b=d"
- (fn _=> [ (SIMP_TAC (FOL_ss addrews [doubleton_iff]) 1),
+ (fn _=> [ (simp_tac (FOL_ss addsimps [doubleton_iff]) 1),
            (fast_tac FOL_cs 1) ]);
 
 val Pair_inject = standard (Pair_iff RS iffD1 RS conjE);
 
 val Pair_inject1 = prove_goal ZF.thy "<a,b> = <c,d> ==> a=c"

     (rtac (major RS SigmaD2) 1) ]);
 
 val Sigma_cong = prove_goalw ZF.thy [Sigma_def]
     "[| A=A';  !!x. x:A' ==> B(x)=B'(x) |] ==> \
 \    Sigma(A,B) = Sigma(A',B')"
- (fn prems=> [ (prove_cong_tac (prems@[RepFun_cong]) 1) ]);
+ (fn prems=> [ (simp_tac (FOL_ss addsimps prems addcongs [RepFun_cong]) 1) ]);
 
 val Sigma_empty1 = prove_goal ZF.thy "Sigma(0,B) = 0"
  (fn _ => [ (fast_tac (lemmas_cs addIs [equalityI] addSEs [SigmaE]) 1) ]);
 
 val Sigma_empty2 = prove_goal ZF.thy "A*0 = 0"

 \    |] ==> split(%x y.c(x,y), p) : C(p)"
  (fn major::prems=>
   [ (rtac (major RS SigmaE) 1),
     (etac ssubst 1),
     (REPEAT (ares_tac (prems @ [split RS ssubst]) 1)) ]);
-
-(*This congruence rule uses NO typing information...*)
-val split_cong = prove_goalw ZF.thy [split_def] 
-    "[| p=p';  !!x y.c(x,y) = c'(x,y) |] ==> \
-\    split(%x y.c(x,y), p) = split(%x y.c'(x,y), p')"
- (fn prems=> [ (prove_cong_tac (prems@[the_cong]) 1) ]);
-
 
 (*** conversions for fst and snd ***)
 
 val fst_conv = prove_goalw ZF.thy [fst_def] "fst(<a,b>) = a"
  (fn _=> [ (rtac split 1) ]);