--- a/src/HOL/Nonstandard_Analysis/NSA.thy Tue Jun 26 14:51:32 2018 +0100
+++ b/src/HOL/Nonstandard_Analysis/NSA.thy Tue Jun 26 15:44:35 2018 +0100
@@ -132,12 +132,6 @@
subsection \<open>Closure Laws for the Standard Reals\<close>
-lemma Reals_minus_iff [simp]: "- x \<in> \<real> \<longleftrightarrow> x \<in> \<real>"
- apply auto
- apply (drule Reals_minus)
- apply auto
- done
-
lemma Reals_add_cancel: "x + y \<in> \<real> \<Longrightarrow> y \<in> \<real> \<Longrightarrow> x \<in> \<real>"
by (drule (1) Reals_diff) simp