# HG changeset patch
# User nipkow
# Date 1550040522 -3600
# Node ID a99a0f5474c5fa95b40e9e6867b148493e09b838
# Parent  74c1a0643010fab3db297c2895ee5057fa29beec
too agressive

diff -r 74c1a0643010 -r a99a0f5474c5 src/HOL/Library/Extended_Nat.thy
--- 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>