# HG changeset patch
# User wenzelm
# Date 1441559360 -7200
# Node ID 65082457c117bd77dde610eed59489739a028c70
# Parent  7beed856816cff21c0da62233e565d123cc150a8
tuned proofs;

diff -r 7beed856816c -r 65082457c117 src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Sun Sep 06 14:51:49 2015 +0200
+++ b/src/HOL/Library/Extended_Real.thy	Sun Sep 06 19:09:20 2015 +0200
@@ -913,7 +913,7 @@
 lemma ereal_times[simp]:
   "1 \<noteq> (\<infinity>::ereal)" "(\<infinity>::ereal) \<noteq> 1"
   "1 \<noteq> -(\<infinity>::ereal)" "-(\<infinity>::ereal) \<noteq> 1"
-  by (auto simp add: times_ereal_def one_ereal_def)
+  by (auto simp: one_ereal_def)
 
 lemma ereal_plus_1[simp]:
   "1 + ereal r = ereal (r + 1)"