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/Real/HahnBanach/Aux.thy
changeset 12481 ea5d6da573c5
parent 12018 ec054019c910
child 13515 a6a7025fd7e8 
--- a/src/HOL/Real/HahnBanach/Aux.thy	Wed Dec 12 19:19:59 2001 +0100
+++ b/src/HOL/Real/HahnBanach/Aux.thy	Wed Dec 12 19:21:02 2001 +0100
@@ -74,7 +74,7 @@
   hence "x * (- z) \<le> y * (- z)"
     by (rule real_mult_le_le_mono2)
   hence  "- (x * z) \<le> - (y * z)"
-    by (simp only: real_minus_mult_eq2)
+    by (simp only: real_mult_minus_eq2)
   thus ?thesis by (simp only: real_mult_commute)
 qed
isabelle