added one more simplification to help replay

--- 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