src/ZF/Order.thy
changeset 9683 f87c8c449018
parent 2469 b50b8c0eec01
child 13119 6f7526467e5a
     1.1 --- a/src/ZF/Order.thy	Thu Aug 24 00:55:42 2000 +0200
     1.2 +++ b/src/ZF/Order.thy	Thu Aug 24 11:05:20 2000 +0200
     1.3 @@ -35,12 +35,15 @@
     1.4  
     1.5    ord_iso_map_def
     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).   
     1.8 -            {<x,y>}"
     1.9 +       UN x:A. UN y:B. UN f: ord_iso(pred(A,x,r), r, pred(B,y,s), s). {<x,y>}"
    1.10  
    1.11  constdefs
    1.12  
    1.13    first :: [i, i, i] => o
    1.14      "first(u, X, R) == u:X & (ALL v:X. v~=u --> <u,v> : R)"
    1.15  
    1.16 +syntax (xsymbols)
    1.17 +    ord_iso :: [i,i,i,i]=>i       ("('(_,_') \\<cong> '(_,_'))" 50)
    1.18 +
    1.19 +
    1.20  end