author avigad Wed, 13 Jul 2005 20:02:54 +0200 changeset 16820 5c9d597e4cb9 parent 16819 00d8f9300d13 child 16821 ba1f6aba44ed
fixed typos in theorem names
```--- a/src/HOL/Real/RComplete.thy	Wed Jul 13 19:49:07 2005 +0200
+++ b/src/HOL/Real/RComplete.thy	Wed Jul 13 20:02:54 2005 +0200
@@ -831,7 +831,7 @@
apply simp
done

-lemma le_natfloor_one_eq [simp]: "(1 <= natfloor x) = (1 <= x)"
+lemma le_natfloor_eq_one [simp]: "(1 <= natfloor x) = (1 <= x)"
apply (case_tac "0 <= x")
apply (subst le_natfloor_eq, assumption, simp)
apply (rule iffI)
@@ -971,13 +971,14 @@
apply (erule natceiling_le)
done

-lemma natceiling_le_eq2 [simp]: "~ neg((number_of n)::int) ==> 0 <= x ==>
-    (natceiling x <= number_of n) = (x <= number_of n)"
+lemma natceiling_le_eq_number_of [simp]:
+    "~ neg((number_of n)::int) ==> 0 <= x ==>
+      (natceiling x <= number_of n) = (x <= number_of n)"
apply (subst natceiling_le_eq, assumption)
apply simp
done

-lemma natceiling_one_le_eq: "(natceiling x <= 1) = (x <= 1)"
+lemma natceiling_le_eq_one: "(natceiling x <= 1) = (x <= 1)"
apply (case_tac "0 <= x")
apply (subst natceiling_le_eq)
apply assumption
@@ -1017,8 +1018,9 @@
apply simp_all
done

-lemma natceiling_add2 [simp]: "~ neg ((number_of n)::int) ==> 0 <= x ==>
-    natceiling (x + number_of n) = natceiling x + number_of n"