changeset 61394 | 6142b282b164 |
parent 61378 | 3e04c9ca001a |
child 61798 | 27f3c10b0b50 |
--- a/src/ZF/Arith.thy Sat Oct 10 22:08:43 2015 +0200 +++ b/src/ZF/Arith.thy Sat Oct 10 22:14:44 2015 +0200 @@ -72,9 +72,6 @@ mod :: "[i,i]=>i" (infixl "mod" 70) where "m mod n == raw_mod (natify(m), natify(n))" -notation (xsymbols) - mult (infixr "#\<times>" 70) - declare rec_type [simp] nat_0_le [simp]