# HG changeset patch
# User berghofe
# Date 939994295 -7200
# Node ID 2e2d7e80fb07c13953c3faf88477651c0418d1c0
# Parent  30fb773113a1139c9b2277dcfd2e81ab04cd820a
Removed obsolete comment.

diff -r 30fb773113a1 -r 2e2d7e80fb07 src/HOL/NatDef.thy
--- a/src/HOL/NatDef.thy	Fri Oct 15 12:31:43 1999 +0200
+++ b/src/HOL/NatDef.thy	Fri Oct 15 15:31:35 1999 +0200
@@ -64,7 +64,7 @@
   Zero_def      "0 == Abs_Nat(Zero_Rep)"
   Suc_def       "Suc == (%n. Abs_Nat(Suc_Rep(Rep_Nat(n))))"
 
-  (*nat operations and recursion*)
+  (*nat operations*)
   pred_nat_def  "pred_nat == {(m,n). n = Suc m}"
 
   less_def      "m<n == (m,n):trancl(pred_nat)"