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.thy
changeset 65885 77d922eff5ac
parent 64267 b9a1486e79be
child 66155 2463cba9f18f 
--- a/src/HOL/Real.thy	Sun May 21 13:00:44 2017 +0200
+++ b/src/HOL/Real.thy	Sun May 21 21:37:31 2017 +0200
@@ -1803,6 +1803,7 @@
   "x + 0 = x"
   "0 * x = 0"
   "1 * x = x"
+  "-x = -1 * x"
   "x + y = y + x"
   for x y :: real
   by auto
isabelle