equal
deleted
inserted
replaced
42 |
42 |
43 Ge :: "(nat*nat) set" |
43 Ge :: "(nat*nat) set" |
44 "Ge == {(x,y). y <= x}" |
44 "Ge == {(x,y). y <= x}" |
45 |
45 |
46 syntax |
46 syntax |
47 pfixLe :: [nat list, nat list] => bool (infixl "pfix'_le" 50) |
47 pfixLe :: [nat list, nat list] => bool (infixl "pfixLe" 50) |
48 pfixGe :: [nat list, nat list] => bool (infixl "pfix'_ge" 50) |
48 pfixGe :: [nat list, nat list] => bool (infixl "pfixGe" 50) |
49 |
49 |
50 translations |
50 translations |
51 "xs pfix_le ys" == "(xs,ys) : genPrefix Le" |
51 "xs pfixLe ys" == "(xs,ys) : genPrefix Le" |
52 |
52 |
53 "xs pfix_ge ys" == "(xs,ys) : genPrefix Ge" |
53 "xs pfixGe ys" == "(xs,ys) : genPrefix Ge" |
54 |
54 |
55 end |
55 end |