diff -r dd58f13a8eb4 -r eb85850d3eb7 src/CTT/Arith.thy
--- a/src/CTT/Arith.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/CTT/Arith.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -13,22 +13,27 @@
 subsection {* Arithmetic operators and their definitions *}
 
 definition
-  add :: "[i,i]=>i"   (infixr "#+" 65)
+  add :: "[i,i]=>i"   (infixr "#+" 65) where
   "a#+b == rec(a, b, %u v. succ(v))"
 
-  diff :: "[i,i]=>i"   (infixr "-" 65)
+definition
+  diff :: "[i,i]=>i"   (infixr "-" 65) where
   "a-b == rec(b, a, %u v. rec(v, 0, %x y. x))"
 
-  absdiff :: "[i,i]=>i"   (infixr "|-|" 65)
+definition
+  absdiff :: "[i,i]=>i"   (infixr "|-|" 65) where
   "a|-|b == (a-b) #+ (b-a)"
 
-  mult :: "[i,i]=>i"   (infixr "#*" 70)
+definition
+  mult :: "[i,i]=>i"   (infixr "#*" 70) where
   "a#*b == rec(a, 0, %u v. b #+ v)"
 
-  mod :: "[i,i]=>i"   (infixr "mod" 70)
+definition
+  mod :: "[i,i]=>i"   (infixr "mod" 70) where
   "a mod b == rec(a, 0, %u v. rec(succ(v) |-| b, 0, %x y. succ(v)))"
 
-  div :: "[i,i]=>i"   (infixr "div" 70)
+definition
+  div :: "[i,i]=>i"   (infixr "div" 70) where
   "a div b == rec(a, 0, %u v. rec(succ(u) mod b, succ(v), %x y. v))"