Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
A single [simp] to handle the case -a/-b.
authorpaulson <lp15@cam.ac.uk>
Sat, 05 Apr 2014 01:04:46 +0100
changeset 56414 c1bbd3e22226
parent 56413 2d4d9a5f68ff
child 56415 f61a0f7cbde5
A single [simp] to handle the case -a/-b.
src/HOL/Fields.thy file | annotate | diff | comparison | revisions 
--- 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