changeset 10467 | e6e7205e9e91 |
parent 3837 | d7f033c74b38 |
child 12110 | f8b4b11cd79d |
--- a/src/CTT/Arith.thy Tue Nov 14 13:25:59 2000 +0100 +++ b/src/CTT/Arith.thy Tue Nov 14 13:26:48 2000 +0100 @@ -14,6 +14,12 @@ consts "#+","-","|-|" :: "[i,i]=>i" (infixr 65) "#*",div,mod :: "[i,i]=>i" (infixr 70) +syntax (symbols) + "op #*" :: [i, i] => i (infixr "#\\<times>" 70) + +syntax (HTML output) + "op #*" :: [i, i] => i (infixr "#\\<times>" 70) + rules add_def "a#+b == rec(a, b, %u v. succ(v))" diff_def "a-b == rec(b, a, %u v. rec(v, 0, %x y. x))"