src/HOL/RComplete.thy
changeset 44708 37ce74ff4203
parent 44707 487ae6317f7b
child 45966 03ce2b2a29a2
     1.1 --- a/src/HOL/RComplete.thy	Sun Sep 04 06:27:59 2011 -0700
     1.2 +++ b/src/HOL/RComplete.thy	Sun Sep 04 06:56:10 2011 -0700
     1.3 @@ -475,12 +475,12 @@
     1.4    unfolding natceiling_def real_of_nat_def
     1.5    by (simp add: nat_le_iff ceiling_le_iff)
     1.6  
     1.7 -lemma natceiling_le_eq: "0 <= x ==> (natceiling x <= a) = (x <= real a)"
     1.8 -  unfolding natceiling_def real_of_nat_def (* FIXME: unused assumption *)
     1.9 +lemma natceiling_le_eq: "(natceiling x <= a) = (x <= real a)"
    1.10 +  unfolding natceiling_def real_of_nat_def
    1.11    by (simp add: nat_le_iff ceiling_le_iff)
    1.12  
    1.13  lemma natceiling_le_eq_number_of [simp]:
    1.14 -    "~ neg((number_of n)::int) ==> 0 <= x ==>
    1.15 +    "~ neg((number_of n)::int) ==>
    1.16        (natceiling x <= number_of n) = (x <= number_of n)"
    1.17    by (simp add: natceiling_le_eq)
    1.18