changeset 12114 | a8e860c86252 |
parent 11321 | 01cbbf33779b |
child 13560 | d9651081578b |
--- a/src/ZF/Integ/Int.thy Fri Nov 09 00:06:15 2001 +0100 +++ b/src/ZF/Integ/Int.thy Fri Nov 09 00:09:47 2001 +0100 @@ -76,7 +76,7 @@ "z1 $<= z2 == z1 $< z2 | intify(z1)=intify(z2)" -syntax (symbols) +syntax (xsymbols) "zmult" :: [i,i] => i (infixl "$\\<times>" 70) "zle" :: [i,i] => o (infixl "$\\<le>" 50) (*less than / equals*)