src/ZF/Arith.thy
changeset 9683 f87c8c449018
parent 9654 9754ba005b64
child 9964 7966a2902266
equal deleted inserted replaced
9682:00f8be1b7209 9683:f87c8c449018
    54     "m div n == raw_div (natify(m), natify(n))"
    54     "m div n == raw_div (natify(m), natify(n))"
    55 
    55 
    56   mod  :: [i,i]=>i                    (infixl "mod" 70)
    56   mod  :: [i,i]=>i                    (infixl "mod" 70)
    57     "m mod n == raw_mod (natify(m), natify(n))"
    57     "m mod n == raw_mod (natify(m), natify(n))"
    58 
    58 
    59 syntax (symbols)
    59 syntax (xsymbols)
    60   "mult"      :: [i, i] => i               (infixr "#\\<times>" 70)
    60   "mult"      :: [i, i] => i               (infixr "#\\<times>" 70)
    61 
    61 
    62 end
    62 end