# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1530024275 -3600
# Node ID 8a8f98c84df3cb9939c516e2d99c958c8b3e2735
# Parent  e3e742b9eed458c56a98d4e8f9edd6e2202ce0d4
deleted redundant theorem

diff -r e3e742b9eed4 -r 8a8f98c84df3 src/HOL/Nonstandard_Analysis/NSA.thy
--- 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