src/ZF/Order.thy
changeset 13615 449a70d88b38
parent 13611 2edf034c902a
child 13701 0a9228532106
     1.1 --- a/src/ZF/Order.thy	Tue Oct 01 11:17:25 2002 +0200
     1.2 +++ b/src/ZF/Order.thy	Tue Oct 01 13:26:10 2002 +0200
     1.3 @@ -38,7 +38,7 @@
     1.4  
     1.5    ord_iso_map :: "[i,i,i,i]=>i"      	(*Construction for linearity theorem*)
     1.6     "ord_iso_map(A,r,B,s) ==
     1.7 -     UN x:A. UN y:B. UN f: ord_iso(pred(A,x,r), r, pred(B,y,s), s). {<x,y>}"
     1.8 +     \<Union>x\<in>A. \<Union>y\<in>B. \<Union>f \<in> ord_iso(pred(A,x,r), r, pred(B,y,s), s). {<x,y>}"
     1.9  
    1.10    first :: "[i, i, i] => o"
    1.11      "first(u, X, R) == u:X & (ALL v:X. v~=u --> <u,v> : R)"