diff -r 6254f50e5ec9 -r a9f7ff3a464c Arith.thy
--- a/Arith.thy	Fri Sep 16 15:48:20 1994 +0200
+++ b/Arith.thy	Wed Sep 21 15:40:41 1994 +0200
@@ -1,24 +1,26 @@
-(*  Title: 	HOL/arith.thy
+(*  Title:      HOL/Arith.thy
     ID:         $Id$
-    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
 Arithmetic operators and their definitions
 *)
 
 Arith = Nat +
-arities nat::plus
-        nat::minus
-        nat::times
+
+instance
+  nat :: {plus, minus, times}
+
 consts
-  pred     :: "nat => nat"
-  div,mod  :: "[nat,nat]=>nat"	(infixl 70)
-rules
+  pred      :: "nat => nat"
+  div, mod  :: "[nat, nat] => nat"  (infixl 70)
+
+defs
   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. pred(v))"  
-  mult_def  "m*n == nat_rec(m, 0, %u v. n + v)"  
-  mod_def   "m mod n == wfrec(trancl(pred_nat), m, %j f. if(j<n, j, f(j-n)))"  
+  add_def   "m+n == nat_rec(m, n, %u v. Suc(v))"
+  diff_def  "m-n == nat_rec(n, m, %u v. pred(v))"
+  mult_def  "m*n == nat_rec(m, 0, %u v. n + v)"
+  mod_def   "m mod n == wfrec(trancl(pred_nat), m, %j f. if(j<n, j, f(j-n)))"
   div_def   "m div n == wfrec(trancl(pred_nat), m, %j f. if(j<n, 0, Suc(f(j-n))))"
 end
 
@@ -26,3 +28,4 @@
   There are no negative numbers; we have
      m - n = 0  iff  m<=n   and     m - n = Suc(k) iff m>n.
   Also, nat_rec(m, 0, %z w.z) is pred(m).   *)
+