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