equal
deleted
inserted
replaced
36 oadd_def "i ++ j == ordertype(i+j, radd(i,Memrel(i),j,Memrel(j)))" |
36 oadd_def "i ++ j == ordertype(i+j, radd(i,Memrel(i),j,Memrel(j)))" |
37 |
37 |
38 (*ordinal subtraction*) |
38 (*ordinal subtraction*) |
39 odiff_def "i -- j == ordertype(i-j, Memrel(i))" |
39 odiff_def "i -- j == ordertype(i-j, Memrel(i))" |
40 |
40 |
41 syntax (symbols) |
41 syntax (xsymbols) |
42 "op **" :: [i,i] => i (infixr "\\<times>\\<times>" 70) |
42 "op **" :: [i,i] => i (infixl "\\<times>\\<times>" 70) |
43 |
43 |
44 end |
44 end |