diff -r 5cd82054c2c6 -r 957bcf55c98f src/CTT/Arith.thy
--- a/src/CTT/Arith.thy	Fri Jun 02 18:15:38 2006 +0200
+++ b/src/CTT/Arith.thy	Fri Jun 02 18:24:48 2006 +0200
@@ -12,27 +12,32 @@
 
 subsection {* Arithmetic operators and their definitions *}
 
-consts
-  "#+"  :: "[i,i]=>i"   (infixr 65)
-  "-"   :: "[i,i]=>i"   (infixr 65)
-  "|-|" :: "[i,i]=>i"   (infixr 65)
-  "#*"  :: "[i,i]=>i"   (infixr 70)
-  div   :: "[i,i]=>i"   (infixr 70)
-  mod   :: "[i,i]=>i"   (infixr 70)
+definition
+  add :: "[i,i]=>i"   (infixr "#+" 65)
+  "a#+b == rec(a, b, %u v. succ(v))"
 
-syntax (xsymbols)
-  "op #*"      :: "[i, i] => i"   (infixr "#\<times>" 70)
+  diff :: "[i,i]=>i"   (infixr "-" 65)
+  "a-b == rec(b, a, %u v. rec(v, 0, %x y. x))"
+
+  absdiff :: "[i,i]=>i"   (infixr "|-|" 65)
+  "a|-|b == (a-b) #+ (b-a)"
+
+  mult :: "[i,i]=>i"   (infixr "#*" 70)
+  "a#*b == rec(a, 0, %u v. b #+ v)"
 
-syntax (HTML output)
-  "op #*"      :: "[i, i] => i"   (infixr "#\<times>" 70)
+  mod :: "[i,i]=>i"   (infixr "mod" 70)
+  "a mod b == rec(a, 0, %u v. rec(succ(v) |-| b, 0, %x y. succ(v)))"
+
+  div :: "[i,i]=>i"   (infixr "div" 70)
+  "a div b == rec(a, 0, %u v. rec(succ(u) mod b, succ(v), %x y. v))"
+
 
-defs
-  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))"
-  absdiff_def: "a|-|b == (a-b) #+ (b-a)"
-  mult_def:    "a#*b == rec(a, 0, %u v. b #+ v)"
-  mod_def:     "a mod b == rec(a, 0, %u v. rec(succ(v) |-| b, 0, %x y. succ(v)))"
-  div_def:     "a div b == rec(a, 0, %u v. rec(succ(u) mod b, succ(v), %x y. v))"
+const_syntax (xsymbols)
+  mult  (infixr "#\<times>" 70)
+
+const_syntax (HTML output)
+  mult (infixr "#\<times>" 70)
+
 
 lemmas arith_defs = add_def diff_def absdiff_def mult_def mod_def div_def