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/Fields.thy
changeset 56414 c1bbd3e22226
parent 56410 a14831ac3023
child 56441 49e95c9ebb59 
--- 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)
isabelle