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

diff -r 8ab69b3e396b -r f55f54a032ce src/ZF/CardinalArith.thy
--- a/src/ZF/CardinalArith.thy	Wed May 03 13:47:24 1995 +0200
+++ b/src/ZF/CardinalArith.thy	Wed May 03 13:55:05 1995 +0200
@@ -27,7 +27,7 @@
   csquare_rel_def
   "csquare_rel(K) ==   \
 \        rvimage(K*K,   \
-\                lam z:K*K. split(%x y. <x Un y, <x,y>>, z), \
+\                lam <x,y>:K*K. <x Un y, x, y>, \
 \                rmult(K,Memrel(K), K*K, rmult(K,Memrel(K), K,Memrel(K))))"
 
   (*This def is more complex than Kunen's but it more easily proved to