# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1396656286 -3600
# Node ID c1bbd3e22226addd8b08f440afee07daa341785e
# Parent  2d4d9a5f68ff191c96e66897f4af847309dc426d
A single [simp] to handle the case -a/-b.

diff -r 2d4d9a5f68ff -r c1bbd3e22226 src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Fri Apr 04 22:51:22 2014 +0200
+++ b/src/HOL/Fields.thy	Sat Apr 05 01:04:46 2014 +0100
@@ -412,7 +412,7 @@
   "a / - b = - (a / b)"
   by (simp add: divide_inverse)
 
-lemma minus_divide_divide:
+lemma minus_divide_divide [simp]:
   "(- a) / (- b) = a / b"
 apply (cases "b=0", simp) 
 apply (simp add: nonzero_minus_divide_divide)