src/ZF/Arith.thy
changeset 12114 a8e860c86252
parent 9964 7966a2902266
child 13163 e320a52ff711
equal deleted inserted replaced
12113:46a14ebdac4f 12114:a8e860c86252
    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 syntax (HTML output)
    62 syntax (HTML output)
    63   "mult"      :: [i, i] => i               (infixr "#\\<times>" 70)
    63   "mult"      :: [i, i] => i               (infixr "#\\<times>" 70)
    64 
    64