author | lcp |
Wed, 03 May 1995 13:55:05 +0200 (1995-05-03) | |
changeset 1091 | f55f54a032ce |
parent 1090 | 8ab69b3e396b |
child 1092 | fdaf39a47a2b |
--- 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