Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Nonstandard_Analysis/HyperNat.thy
changeset 70228 2d5b122aa0ff
parent 70219 b21efbf64292 
--- a/src/HOL/Nonstandard_Analysis/HyperNat.thy	Thu May 02 11:43:56 2019 +0200
+++ b/src/HOL/Nonstandard_Analysis/HyperNat.thy	Thu May 02 12:58:32 2019 +0100
@@ -234,9 +234,6 @@
 lemma HNatInfinite_add: "x \<in> HNatInfinite \<Longrightarrow> x + y \<in> HNatInfinite"
   using HNatInfinite_upward_closed hypnat_le_add1 by blast
 
-lemma HNatInfinite_add_one: "x \<in> HNatInfinite \<Longrightarrow> x + 1 \<in> HNatInfinite"
-  by (rule HNatInfinite_add)
-
 lemma HNatInfinite_diff: "\<lbrakk>x \<in> HNatInfinite; y \<in> Nats\<rbrakk> \<Longrightarrow> x - y \<in> HNatInfinite"
   by (metis HNatInfinite_not_Nats_iff Nats_add Nats_le_HNatInfinite le_add_diff_inverse)
isabelle