src/HOL/Library/Extended_Nat.thy
changeset 57512 cc97b347b301
parent 56777 9c3f0ae99532
child 57514 bdc2c6b40bf2
     1.1 --- a/src/HOL/Library/Extended_Nat.thy	Fri Jul 04 20:07:08 2014 +0200
     1.2 +++ b/src/HOL/Library/Extended_Nat.thy	Fri Jul 04 20:18:47 2014 +0200
     1.3 @@ -175,7 +175,7 @@
     1.4    by (simp_all add: eSuc_plus_1 add_ac)
     1.5  
     1.6  lemma iadd_Suc_right: "m + eSuc n = eSuc (m + n)"
     1.7 -  by (simp only: add_commute[of m] iadd_Suc)
     1.8 +  by (simp only: add.commute[of m] iadd_Suc)
     1.9  
    1.10  lemma iadd_is_0: "(m + n = (0::enat)) = (m = 0 \<and> n = 0)"
    1.11    by (cases m, cases n, simp_all add: zero_enat_def)