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/SupInf.thy
changeset 37887 2ae085b07f2f
parent 37765 26bdfb7b680b
child 44669 8e6cdb9c00a7 
--- a/src/HOL/SupInf.thy	Mon Jul 19 16:09:44 2010 +0200
+++ b/src/HOL/SupInf.thy	Mon Jul 19 16:09:44 2010 +0200
@@ -417,7 +417,7 @@
   also have "... \<le> e" 
     apply (rule Sup_asclose) 
     apply (auto simp add: S)
-    apply (metis abs_minus_add_cancel b add_commute diff_def)
+    apply (metis abs_minus_add_cancel b add_commute diff_minus)
     done
   finally have "\<bar>- Sup (uminus ` S) - l\<bar> \<le> e" .
   thus ?thesis
isabelle