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