fixed typos in theorem names
authoravigad
Wed Jul 13 20:02:54 2005 +0200 (2005-07-13)
changeset 168205c9d597e4cb9
parent 16819 00d8f9300d13
child 16821 ba1f6aba44ed
fixed typos in theorem names
src/HOL/Real/RComplete.thy
     1.1 --- a/src/HOL/Real/RComplete.thy	Wed Jul 13 19:49:07 2005 +0200
     1.2 +++ b/src/HOL/Real/RComplete.thy	Wed Jul 13 20:02:54 2005 +0200
     1.3 @@ -831,7 +831,7 @@
     1.4    apply simp
     1.5  done
     1.6  
     1.7 -lemma le_natfloor_one_eq [simp]: "(1 <= natfloor x) = (1 <= x)"
     1.8 +lemma le_natfloor_eq_one [simp]: "(1 <= natfloor x) = (1 <= x)"
     1.9    apply (case_tac "0 <= x")
    1.10    apply (subst le_natfloor_eq, assumption, simp)
    1.11    apply (rule iffI)
    1.12 @@ -971,13 +971,14 @@
    1.13    apply (erule natceiling_le)
    1.14  done
    1.15  
    1.16 -lemma natceiling_le_eq2 [simp]: "~ neg((number_of n)::int) ==> 0 <= x ==>
    1.17 -    (natceiling x <= number_of n) = (x <= number_of n)"
    1.18 +lemma natceiling_le_eq_number_of [simp]: 
    1.19 +    "~ neg((number_of n)::int) ==> 0 <= x ==>
    1.20 +      (natceiling x <= number_of n) = (x <= number_of n)"
    1.21    apply (subst natceiling_le_eq, assumption)
    1.22    apply simp
    1.23  done
    1.24  
    1.25 -lemma natceiling_one_le_eq: "(natceiling x <= 1) = (x <= 1)"
    1.26 +lemma natceiling_le_eq_one: "(natceiling x <= 1) = (x <= 1)"
    1.27    apply (case_tac "0 <= x")
    1.28    apply (subst natceiling_le_eq)
    1.29    apply assumption
    1.30 @@ -1017,8 +1018,9 @@
    1.31    apply simp_all
    1.32  done
    1.33  
    1.34 -lemma natceiling_add2 [simp]: "~ neg ((number_of n)::int) ==> 0 <= x ==> 
    1.35 -    natceiling (x + number_of n) = natceiling x + number_of n"
    1.36 +lemma natceiling_add_number_of [simp]: 
    1.37 +    "~ neg ((number_of n)::int) ==> 0 <= x ==> 
    1.38 +      natceiling (x + number_of n) = natceiling x + number_of n"
    1.39    apply (subst natceiling_add [THEN sym])
    1.40    apply simp_all
    1.41  done