src/ZF/CardinalArith.thy
changeset 32960 69916a850301
parent 27517 c055e1d49285
child 39159 0dec18004e75
     1.1 --- a/src/ZF/CardinalArith.thy	Sat Oct 17 01:05:59 2009 +0200
     1.2 +++ b/src/ZF/CardinalArith.thy	Sat Oct 17 14:43:18 2009 +0200
     1.3 @@ -1,8 +1,6 @@
     1.4  (*  Title:      ZF/CardinalArith.thy
     1.5 -    ID:         $Id$
     1.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7      Copyright   1994  University of Cambridge
     1.8 -
     1.9  *)
    1.10  
    1.11  header{*Cardinal Arithmetic Without the Axiom of Choice*}
    1.12 @@ -24,9 +22,9 @@
    1.13  definition
    1.14    csquare_rel   :: "i=>i"  where
    1.15      "csquare_rel(K) ==   
    1.16 -	  rvimage(K*K,   
    1.17 -		  lam <x,y>:K*K. <x Un y, x, y>, 
    1.18 -		  rmult(K,Memrel(K), K*K, rmult(K,Memrel(K), K,Memrel(K))))"
    1.19 +          rvimage(K*K,   
    1.20 +                  lam <x,y>:K*K. <x Un y, x, y>, 
    1.21 +                  rmult(K,Memrel(K), K*K, rmult(K,Memrel(K), K,Memrel(K))))"
    1.22  
    1.23  definition
    1.24    jump_cardinal :: "i=>i"  where