| changeset 30102 | 799b687e4aac |
| parent 30096 | c5497842ee35 |
| child 35028 | 108662d50512 |
--- a/src/HOL/Archimedean_Field.thy Wed Feb 25 11:30:46 2009 -0800 +++ b/src/HOL/Archimedean_Field.thy Thu Feb 26 06:21:31 2009 -0800 @@ -391,10 +391,10 @@ subsection {* Negation *} -lemma floor_minus [simp]: "floor (- x) = - ceiling x" +lemma floor_minus: "floor (- x) = - ceiling x" unfolding ceiling_def by simp -lemma ceiling_minus [simp]: "ceiling (- x) = - floor x" +lemma ceiling_minus: "ceiling (- x) = - floor x" unfolding ceiling_def by simp end