# HG changeset patch
# User nipkow
# Date 1470464818 -7200
# Node ID 854402aa9374948fb1685e63c9e368cc7ae1414b
# Parent  f1cae4239d4c2293321c8019b6208a215f5351af
tuned

diff -r f1cae4239d4c -r 854402aa9374 src/HOL/Archimedean_Field.thy
--- a/src/HOL/Archimedean_Field.thy	Fri Aug 05 22:25:32 2016 +0200
+++ b/src/HOL/Archimedean_Field.thy	Sat Aug 06 08:26:58 2016 +0200
@@ -640,8 +640,8 @@
   ultimately show ?thesis by (auto simp add: frac_def algebra_simps)
 qed
 
-lemma floor_add2[simp]: "frac x = 0 \<or> frac y = 0 \<Longrightarrow> \<lfloor>x + y\<rfloor> = \<lfloor>x\<rfloor> + \<lfloor>y\<rfloor>"
-by (metis add.commute add.left_neutral frac_lt_1 floor_add)
+lemma floor_add2[simp]: "x \<in> \<int> \<or> y \<in> \<int> \<Longrightarrow> \<lfloor>x + y\<rfloor> = \<lfloor>x\<rfloor> + \<lfloor>y\<rfloor>"
+by (metis add.commute add.left_neutral frac_lt_1 floor_add frac_eq_0_iff)
 
 lemma frac_add:
   "frac (x + y) = (if frac x + frac y < 1 then frac x + frac y else (frac x + frac y) - 1)"