# HG changeset patch
# User lcp
# Date 799501644 -7200
# Node ID 8ab69b3e396bccebe906935b44813177e67ecfb2
# Parent  e679617661bc3d72d5cc4694c455d50c0435246f
Changed some definitions and proofs to use pattern-matching.

diff -r e679617661bc -r 8ab69b3e396b src/ZF/CardinalArith.ML
--- a/src/ZF/CardinalArith.ML	Wed May 03 13:40:19 1995 +0200
+++ b/src/ZF/CardinalArith.ML	Wed May 03 13:47:24 1995 +0200
@@ -168,7 +168,7 @@
 (*Easier to prove the two directions separately*)
 goalw CardinalArith.thy [eqpoll_def] "A*B eqpoll B*A";
 by (rtac exI 1);
-by (res_inst_tac [("c", "split(%x y.<y,x>)"), ("d", "split(%x y.<y,x>)")] 
+by (res_inst_tac [("c", "%<x,y>.<y,x>"), ("d", "%<x,y>.<y,x>")] 
     lam_bijective 1);
 by (safe_tac ZF_cs);
 by (ALLGOALS (asm_simp_tac ZF_ss));
@@ -278,8 +278,8 @@
 goalw CardinalArith.thy [lepoll_def]
      "!!A B C D. [| A lepoll C;  B lepoll D |] ==> A * B  lepoll  C * D";
 by (REPEAT (etac exE 1));
-by (res_inst_tac [("x", "lam z:A*B. split(%w y.<f`w, fa`y>, z)")] exI 1);
-by (res_inst_tac [("d", "split(%w y.<converse(f)`w, converse(fa)`y>)")] 
+by (res_inst_tac [("x", "lam <w,y>:A*B. <f`w, fa`y>")] exI 1);
+by (res_inst_tac [("d", "%<w,y>.<converse(f)`w, converse(fa)`y>")] 
 		  lam_injective 1);
 by (typechk_tac (inj_is_fun::ZF_typechecks));
 by (etac SigmaE 1);
@@ -298,7 +298,7 @@
 
 goalw CardinalArith.thy [eqpoll_def] "succ(A)*B eqpoll B + A*B";
 by (rtac exI 1);
-by (res_inst_tac [("c", "split(%x y. if(x=A, Inl(y), Inr(<x,y>)))"), 
+by (res_inst_tac [("c", "%<x,y>. if(x=A, Inl(y), Inr(<x,y>))"), 
 		  ("d", "case(%y. <A,y>, %z.z)")] 
     lam_bijective 1);
 by (safe_tac (ZF_cs addSEs [sumE]));
@@ -410,8 +410,7 @@
 (** Establishing the well-ordering **)
 
 goalw CardinalArith.thy [inj_def]
- "!!K. Ord(K) ==>	\
-\ (lam z:K*K. split(%x y. <x Un y, <x, y>>, z)) : inj(K*K, K*K*K)";
+ "!!K. Ord(K) ==> (lam <x,y>:K*K. <x Un y, x, y>) : inj(K*K, K*K*K)";
 by (fast_tac (ZF_cs addss ZF_ss
 		    addIs [lam_type, Un_least_lt RS ltD, ltI]) 1);
 qed "csquare_lam_inj";