src/HOL/Nat_Numeral.thy
changeset 31790 05c92381363c
parent 31182 7ac0a57a57ed
child 31998 2c7a24f74db9
     1.1 --- a/src/HOL/Nat_Numeral.thy	Tue Jun 23 21:07:39 2009 +0200
     1.2 +++ b/src/HOL/Nat_Numeral.thy	Wed Jun 24 09:41:14 2009 +0200
     1.3 @@ -521,10 +521,10 @@
     1.4  
     1.5  subsubsection{*Arith *}
     1.6  
     1.7 -lemma Suc_eq_add_numeral_1: "Suc n = n + 1"
     1.8 +lemma Suc_eq_plus1: "Suc n = n + 1"
     1.9  by (simp add: numerals)
    1.10  
    1.11 -lemma Suc_eq_add_numeral_1_left: "Suc n = 1 + n"
    1.12 +lemma Suc_eq_plus1_left: "Suc n = 1 + n"
    1.13  by (simp add: numerals)
    1.14  
    1.15  (* These two can be useful when m = number_of... *)