| changeset 13119 | 6f7526467e5a |
| parent 9683 | f87c8c449018 |
| child 13140 | 6d97dbb189a9 |
| 13118:336b0bcbd27c | 13119:6f7526467e5a |
|---|---|
41 |
41 |
42 first :: [i, i, i] => o |
42 first :: [i, i, i] => o |
43 "first(u, X, R) == u:X & (ALL v:X. v~=u --> <u,v> : R)" |
43 "first(u, X, R) == u:X & (ALL v:X. v~=u --> <u,v> : R)" |
44 |
44 |
45 syntax (xsymbols) |
45 syntax (xsymbols) |
46 ord_iso :: [i,i,i,i]=>i ("('(_,_') \\<cong> '(_,_'))" 50) |
46 ord_iso :: [i,i,i,i]=>i ("(\\<langle>_, _\\<rangle> \\<cong>/ \\<langle>_, _\\<rangle>)" 51) |
47 |
47 |
48 |
48 |
49 end |
49 end |