equal
deleted
inserted
replaced
69 "m div n == raw_div (natify(m), natify(n))" |
69 "m div n == raw_div (natify(m), natify(n))" |
70 |
70 |
71 definition |
71 definition |
72 mod :: "[i,i]=>i" (infixl "mod" 70) where |
72 mod :: "[i,i]=>i" (infixl "mod" 70) where |
73 "m mod n == raw_mod (natify(m), natify(n))" |
73 "m mod n == raw_mod (natify(m), natify(n))" |
74 |
|
75 notation (xsymbols) |
|
76 mult (infixr "#\<times>" 70) |
|
77 |
74 |
78 declare rec_type [simp] |
75 declare rec_type [simp] |
79 nat_0_le [simp] |
76 nat_0_le [simp] |
80 |
77 |
81 |
78 |