equal
deleted
inserted
replaced
30 |
30 |
31 div :: "[i,i]=>i" (infixr "div" 70) |
31 div :: "[i,i]=>i" (infixr "div" 70) |
32 "a div b == rec(a, 0, %u v. rec(succ(u) mod b, succ(v), %x y. v))" |
32 "a div b == rec(a, 0, %u v. rec(succ(u) mod b, succ(v), %x y. v))" |
33 |
33 |
34 |
34 |
35 const_syntax (xsymbols) |
35 notation (xsymbols) |
36 mult (infixr "#\<times>" 70) |
36 mult (infixr "#\<times>" 70) |
37 |
37 |
38 const_syntax (HTML output) |
38 notation (HTML output) |
39 mult (infixr "#\<times>" 70) |
39 mult (infixr "#\<times>" 70) |
40 |
40 |
41 |
41 |
42 lemmas arith_defs = add_def diff_def absdiff_def mult_def mod_def div_def |
42 lemmas arith_defs = add_def diff_def absdiff_def mult_def mod_def div_def |
43 |
43 |