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/Library/Extended_Nonnegative_Real.thy
changeset 67452 aab817885622
parent 67451 12bcfbac45a1
child 67456 7895c159d7b1 
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy	Wed Jan 17 09:55:03 2018 +0100
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy	Wed Jan 17 12:27:06 2018 +0100
@@ -659,9 +659,6 @@
   subgoal for a b c
     apply (cases a b c rule: ereal3_cases)
     apply (auto simp: ereal_max[symmetric] simp del: ereal_max)
-    apply (auto simp: top_ereal_def[symmetric] sup_ereal_def[symmetric]
-                simp del: sup_ereal_def)
-    apply (auto simp add: top_ereal_def)
     done
   done
isabelle