# HG changeset patch
# User lcp
# Date 788196544 -3600
# Node ID aa332949ce1a0078b53842d898b696dce5ece0b1
# Parent  190974c664a381010ffd39d9dd7fd4ad9ae18cc9
csquare_rel_def: renamed k to K

diff -r 190974c664a3 -r aa332949ce1a src/ZF/CardinalArith.thy
--- a/src/ZF/CardinalArith.thy	Fri Dec 23 16:28:26 1994 +0100
+++ b/src/ZF/CardinalArith.thy	Fri Dec 23 16:29:04 1994 +0100
@@ -9,25 +9,26 @@
 CardinalArith = Cardinal + OrderArith + Arith + Finite + 
 consts
 
-  InfCard     :: "i=>o"
-  "|*|"       :: "[i,i]=>i"       (infixl 70)
-  "|+|"       :: "[i,i]=>i"       (infixl 65)
-  csquare_rel :: "i=>i"
+  InfCard       :: "i=>o"
+  "|*|"         :: "[i,i]=>i"       (infixl 70)
+  "|+|"         :: "[i,i]=>i"       (infixl 65)
+  csquare_rel   :: "i=>i"
   jump_cardinal :: "i=>i"
-  csucc       :: "i=>i"
+  csucc         :: "i=>i"
 
 defs
 
   InfCard_def  "InfCard(i) == Card(i) & nat le i"
 
-  cadd_def     "i |+| j == | i+j |"
+  cadd_def     "i |+| j == |i+j|"
 
-  cmult_def    "i |*| j == | i*j |"
+  cmult_def    "i |*| j == |i*j|"
 
   csquare_rel_def
-  "csquare_rel(k) == rvimage(k*k, lam z:k*k. split(%x y. <x Un y, <x,y>>, z), \
-\                            rmult(k,Memrel(k), k*k, 	\
-\                                  rmult(k,Memrel(k), k,Memrel(k))))"
+  "csquare_rel(K) ==   \
+\        rvimage(K*K,   \
+\                lam z:K*K. split(%x y. <x Un y, <x,y>>, z), \
+\                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
     be a cardinal*)