# HG changeset patch
# User huffman
# Date 1322028001 -3600
# Node ID c05e8209a3aa07022b49153be237c685f05cd9d5
# Parent  e19788cb0a1ab104cfabb4acd04eae87e9884eb8
remove outdated comment

diff -r e19788cb0a1a -r c05e8209a3aa src/HOL/ex/BinEx.thy
--- a/src/HOL/ex/BinEx.thy	Mon Nov 21 23:29:53 2011 +0100
+++ b/src/HOL/ex/BinEx.thy	Wed Nov 23 07:00:01 2011 +0100
@@ -280,8 +280,7 @@
 text {* Successor *}
 
 lemma "Suc 99999 = 100000"
-  by (simp add: Suc_nat_number_of)
-    -- {* not a default rewrite since sometimes we want to have @{text "Suc nnn"} *}
+  by simp
 
 
 text {* \medskip Addition *}