Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
too agressive
authornipkow
Wed, 13 Feb 2019 07:48:42 +0100
changeset 69801 a99a0f5474c5
parent 69800 74c1a0643010
child 69802 6ec272e153f0
too agressive
src/HOL/Library/Extended_Nat.thy file | annotate | diff | comparison | revisions 
--- 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>
isabelle