Changed some definitions and proofs to use pattern-matching.
authorlcp
Wed May 03 13:55:05 1995 +0200 (1995-05-03)
changeset 1091f55f54a032ce
parent 1090 8ab69b3e396b
child 1092 fdaf39a47a2b
Changed some definitions and proofs to use pattern-matching.
src/ZF/CardinalArith.thy
     1.1 --- a/src/ZF/CardinalArith.thy	Wed May 03 13:47:24 1995 +0200
     1.2 +++ b/src/ZF/CardinalArith.thy	Wed May 03 13:55:05 1995 +0200
     1.3 @@ -27,7 +27,7 @@
     1.4    csquare_rel_def
     1.5    "csquare_rel(K) ==   \
     1.6  \        rvimage(K*K,   \
     1.7 -\                lam z:K*K. split(%x y. <x Un y, <x,y>>, z), \
     1.8 +\                lam <x,y>:K*K. <x Un y, x, y>, \
     1.9  \                rmult(K,Memrel(K), K*K, rmult(K,Memrel(K), K,Memrel(K))))"
    1.10  
    1.11    (*This def is more complex than Kunen's but it more easily proved to