# HG changeset patch
# User nipkow
# Date 860088723 -7200
# Node ID 00b8ee790d89866a1ecb995a68d2bf98ab1819a1
# Parent  fd5645efa43d1c057d340b0f42428eadbc0412f6
Only layout mods.

diff -r fd5645efa43d -r 00b8ee790d89 src/HOL/Arith.thy
--- a/src/HOL/Arith.thy	Thu Apr 03 19:29:53 1997 +0200
+++ b/src/HOL/Arith.thy	Thu Apr 03 19:32:03 1997 +0200
@@ -23,25 +23,16 @@
   div_def   "m div n == wfrec (trancl pred_nat) 
                           (%f j. if j<n then 0 else Suc (f (j-n))) m"
 
-
 primrec "op +" nat 
-"0 + n = n"
-"Suc m + n = Suc(m + n)"
-
+  "0 + n = n"
+  "Suc m + n = Suc(m + n)"
 
 primrec "op -" nat 
-"m - 0 = m"
-"m - Suc n = pred(m - n)"
+  "m - 0 = m"
+  "m - Suc n = pred(m - n)"
 
 primrec "op *"  nat 
-"0 * n = 0"
-"Suc m * n = n + (m * n)"
-
+  "0 * n = 0"
+  "Suc m * n = n + (m * 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(0, %z w.z, m) is pred(m).   *)
-