too agressive
authornipkow
Wed Feb 13 07:48:42 2019 +0100 (6 days ago)
changeset 69801a99a0f5474c5
parent 69800 74c1a0643010
child 69802 6ec272e153f0
too agressive
src/HOL/Library/Extended_Nat.thy
     1.1 --- a/src/HOL/Library/Extended_Nat.thy	Wed Feb 13 02:13:46 2019 +0100
     1.2 +++ b/src/HOL/Library/Extended_Nat.thy	Wed Feb 13 07:48:42 2019 +0100
     1.3 @@ -531,7 +531,7 @@
     1.4  lemma enat_add_left_cancel_less: "a + b < a + c \<longleftrightarrow> a \<noteq> (\<infinity>::enat) \<and> b < c"
     1.5    unfolding plus_enat_def by (simp split: enat.split)
     1.6  
     1.7 -lemma plus_eq_infty_iff_enat[simp]: "(m::enat) + n = \<infinity> \<longleftrightarrow> m=\<infinity> \<or> n=\<infinity>"
     1.8 +lemma plus_eq_infty_iff_enat: "(m::enat) + n = \<infinity> \<longleftrightarrow> m=\<infinity> \<or> n=\<infinity>"
     1.9  using enat_add_left_cancel by fastforce
    1.10  
    1.11  ML \<open>