Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/ZF/CardinalArith.thy
changeset 1091 f55f54a032ce
parent 827 aa332949ce1a
child 1155 928a16e02f9f 
--- 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
isabelle