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.
tuned proofs;
authorwenzelm
Sun, 06 Sep 2015 19:09:20 +0200
changeset 61120 65082457c117
parent 61119 7beed856816c
child 61121 efe8b18306b7
tuned proofs;
src/HOL/Library/Extended_Real.thy file | annotate | diff | comparison | revisions 
--- 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)"
isabelle