# 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 \ frac y = 0 \ \x + y\ = \x\ + \y\" -by (metis add.commute add.left_neutral frac_lt_1 floor_add) +lemma floor_add2[simp]: "x \ \ \ y \ \ \ \x + y\ = \x\ + \y\" +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)"