src/ZF/Pair.ML
changeset 6 8ce8c4d13d4d
parent 0 a5a9c433f639
     1.1 --- a/src/ZF/Pair.ML	Fri Sep 17 12:53:53 1993 +0200
     1.2 +++ b/src/ZF/Pair.ML	Fri Sep 17 16:16:38 1993 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4  
     1.5  val Pair_iff = prove_goalw ZF.thy [Pair_def]
     1.6      "<a,b> = <c,d> <-> a=c & b=d"
     1.7 - (fn _=> [ (SIMP_TAC (FOL_ss addrews [doubleton_iff]) 1),
     1.8 + (fn _=> [ (simp_tac (FOL_ss addsimps [doubleton_iff]) 1),
     1.9             (fast_tac FOL_cs 1) ]);
    1.10  
    1.11  val Pair_inject = standard (Pair_iff RS iffD1 RS conjE);
    1.12 @@ -89,7 +89,7 @@
    1.13  val Sigma_cong = prove_goalw ZF.thy [Sigma_def]
    1.14      "[| A=A';  !!x. x:A' ==> B(x)=B'(x) |] ==> \
    1.15  \    Sigma(A,B) = Sigma(A',B')"
    1.16 - (fn prems=> [ (prove_cong_tac (prems@[RepFun_cong]) 1) ]);
    1.17 + (fn prems=> [ (simp_tac (FOL_ss addsimps prems addcongs [RepFun_cong]) 1) ]);
    1.18  
    1.19  val Sigma_empty1 = prove_goal ZF.thy "Sigma(0,B) = 0"
    1.20   (fn _ => [ (fast_tac (lemmas_cs addIs [equalityI] addSEs [SigmaE]) 1) ]);
    1.21 @@ -114,13 +114,6 @@
    1.22      (etac ssubst 1),
    1.23      (REPEAT (ares_tac (prems @ [split RS ssubst]) 1)) ]);
    1.24  
    1.25 -(*This congruence rule uses NO typing information...*)
    1.26 -val split_cong = prove_goalw ZF.thy [split_def] 
    1.27 -    "[| p=p';  !!x y.c(x,y) = c'(x,y) |] ==> \
    1.28 -\    split(%x y.c(x,y), p) = split(%x y.c'(x,y), p')"
    1.29 - (fn prems=> [ (prove_cong_tac (prems@[the_cong]) 1) ]);
    1.30 -
    1.31 -
    1.32  (*** conversions for fst and snd ***)
    1.33  
    1.34  val fst_conv = prove_goalw ZF.thy [fst_def] "fst(<a,b>) = a"