src/HOL/Archimedean_Field.thy
changeset 30102 799b687e4aac
parent 30096 c5497842ee35
child 35028 108662d50512
     1.1 --- a/src/HOL/Archimedean_Field.thy	Wed Feb 25 11:30:46 2009 -0800
     1.2 +++ b/src/HOL/Archimedean_Field.thy	Thu Feb 26 06:21:31 2009 -0800
     1.3 @@ -391,10 +391,10 @@
     1.4  
     1.5  subsection {* Negation *}
     1.6  
     1.7 -lemma floor_minus [simp]: "floor (- x) = - ceiling x"
     1.8 +lemma floor_minus: "floor (- x) = - ceiling x"
     1.9    unfolding ceiling_def by simp
    1.10  
    1.11 -lemma ceiling_minus [simp]: "ceiling (- x) = - floor x"
    1.12 +lemma ceiling_minus: "ceiling (- x) = - floor x"
    1.13    unfolding ceiling_def by simp
    1.14  
    1.15  end