diff -r f04b33ce250f -r a4dc62a46ee4 Arith.thy
--- a/Arith.thy	Tue Oct 24 14:59:17 1995 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,31 +0,0 @@
-(*  Title:      HOL/Arith.thy
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1993  University of Cambridge
-
-Arithmetic operators and their definitions
-*)
-
-Arith = Nat +
-
-instance
-  nat :: {plus, minus, times}
-
-consts
-  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)))"
-  div_def   "m div n == wfrec(trancl(pred_nat), m, %j f. if(j<n, 0, Suc(f(j-n))))"
-end
-
-(*"Difference" is subtraction of natural numbers.
-  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).   *)
-