src/HOL/Library/Extended_Nat.thy
changeset 69801 a99a0f5474c5
parent 69800 74c1a0643010
child 69803 a24865b6262f
--- a/src/HOL/Library/Extended_Nat.thy	Wed Feb 13 02:13:46 2019 +0100
+++ b/src/HOL/Library/Extended_Nat.thy	Wed Feb 13 07:48:42 2019 +0100
@@ -531,7 +531,7 @@
 lemma enat_add_left_cancel_less: "a + b < a + c \<longleftrightarrow> a \<noteq> (\<infinity>::enat) \<and> b < c"
   unfolding plus_enat_def by (simp split: enat.split)
 
-lemma plus_eq_infty_iff_enat[simp]: "(m::enat) + n = \<infinity> \<longleftrightarrow> m=\<infinity> \<or> n=\<infinity>"
+lemma plus_eq_infty_iff_enat: "(m::enat) + n = \<infinity> \<longleftrightarrow> m=\<infinity> \<or> n=\<infinity>"
 using enat_add_left_cancel by fastforce
 
 ML \<open>