src/ZF/CardinalArith.ML
 changeset 1090 8ab69b3e396b parent 1075 848bf2e18dff child 1461 6bcb44e4d6e5
```--- 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);