--- a/arith.thy	Mon Nov 29 18:35:02 1993 +0100
+++ b/arith.thy	Tue Nov 30 17:44:04 1993 +0100
@@ -11,8 +11,10 @@
         nat::minus
         nat::times
 consts
+  pred     :: "nat => nat"
   div,mod  :: "[nat,nat]=>nat"	(infixl 70)
 rules
+  pred_def  "pred(m) == nat_rec(m, 0, %n r.n)"
   add_def   "m+n == nat_rec(m, n, %u v.Suc(v))"  
   diff_def  "m-n == nat_rec(n, m, %u v. nat_rec(v, 0, %x y.x))"  
   mult_def  "m*n == nat_rec(m, 0, %u v. n + v)"