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/Rat.thy
changeset 56571 f4635657d66f
parent 56544 b60d5d119489
child 57136 653e56c6c963 
--- a/src/HOL/Rat.thy	Mon Apr 14 10:55:56 2014 +0200
+++ b/src/HOL/Rat.thy	Mon Apr 14 13:08:17 2014 +0200
@@ -578,7 +578,7 @@
     by (cases "b = 0", simp, simp add: of_int_rat)
   moreover have "0 \<le> Fract (a mod b) b \<and> Fract (a mod b) b < 1"
     unfolding Fract_of_int_quotient
-    by (rule linorder_cases [of b 0]) (simp add: divide_nonpos_neg, simp, simp add: divide_nonneg_pos)
+    by (rule linorder_cases [of b 0]) (simp_all add: divide_nonpos_neg)
   ultimately show ?thesis by simp
 qed
isabelle