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/Library/Fraction_Field.thy
changeset 54230 b1d955791529
parent 53374 a14d2a854c02
child 54463 faad28e65b48 
--- a/src/HOL/Library/Fraction_Field.thy	Thu Oct 31 16:54:22 2013 +0100
+++ b/src/HOL/Library/Fraction_Field.thy	Fri Nov 01 18:51:14 2013 +0100
@@ -132,7 +132,7 @@
 lemma diff_fract [simp]:
   assumes "b \<noteq> 0" and "d \<noteq> 0"
   shows "Fract a b - Fract c d = Fract (a * d - c * b) (b * d)"
-  using assms by (simp add: diff_fract_def diff_minus)
+  using assms by (simp add: diff_fract_def)
 
 definition mult_fract_def:
   "q * r = Abs_fract (\<Union>x \<in> Rep_fract q. \<Union>y \<in> Rep_fract r.
isabelle