# HG changeset patch # User huffman # Date 1333024176 -7200 # Node ID 9ae03b37b4f647c201121d987acb1147a90bb59d # Parent 0c0501cb6da6fd5d1bd2dd8de969fe42dd8ef783 remove duplicate lemma Suc_numeral diff -r 0c0501cb6da6 -r 9ae03b37b4f6 src/HOL/Nat_Numeral.thy --- a/src/HOL/Nat_Numeral.thy Thu Mar 29 14:09:10 2012 +0200 +++ b/src/HOL/Nat_Numeral.thy Thu Mar 29 14:29:36 2012 +0200 @@ -40,10 +40,6 @@ "Suc (numeral v + n) = numeral (v + Num.One) + n" by simp -lemma Suc_numeral [simp]: - "Suc (numeral v) = numeral (v + Num.One)" - by simp - subsubsection{*Subtraction *}