src/CTT/Arith.thy
changeset 21210 c17fd2df4e9e
parent 19762 957bcf55c98f
child 21404 eb85850d3eb7
     1.1 --- a/src/CTT/Arith.thy	Tue Nov 07 11:47:56 2006 +0100
     1.2 +++ b/src/CTT/Arith.thy	Tue Nov 07 11:47:57 2006 +0100
     1.3 @@ -32,10 +32,10 @@
     1.4    "a div b == rec(a, 0, %u v. rec(succ(u) mod b, succ(v), %x y. v))"
     1.5  
     1.6  
     1.7 -const_syntax (xsymbols)
     1.8 +notation (xsymbols)
     1.9    mult  (infixr "#\<times>" 70)
    1.10  
    1.11 -const_syntax (HTML output)
    1.12 +notation (HTML output)
    1.13    mult (infixr "#\<times>" 70)
    1.14  
    1.15