# HG changeset patch
# User blanchet
# Date 1495395451 -7200
# Node ID 77d922eff5acceb58f811e95fac4c53d35b413e2
# Parent  d76937b773d9fc8f47f9ddb76a9649636d24c94c
added one more simplification to help replay

diff -r d76937b773d9 -r 77d922eff5ac src/HOL/Real.thy
--- 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