| changeset 21210 | c17fd2df4e9e |
| parent 19762 | 957bcf55c98f |
| child 21404 | eb85850d3eb7 |
--- a/src/CTT/Arith.thy Tue Nov 07 11:47:56 2006 +0100 +++ b/src/CTT/Arith.thy Tue Nov 07 11:47:57 2006 +0100 @@ -32,10 +32,10 @@ "a div b == rec(a, 0, %u v. rec(succ(u) mod b, succ(v), %x y. v))" -const_syntax (xsymbols) +notation (xsymbols) mult (infixr "#\<times>" 70) -const_syntax (HTML output) +notation (HTML output) mult (infixr "#\<times>" 70)