# HG changeset patch
# User avigad
# Date 1121277774 -7200
# Node ID 5c9d597e4cb910d5398acea024451e85dacc0afe
# Parent  00d8f9300d13d6418f5c9e6f1e0a479d3dc5bd33
fixed typos in theorem names

diff -r 00d8f9300d13 -r 5c9d597e4cb9 src/HOL/Real/RComplete.thy
--- 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"
+lemma natceiling_add_number_of [simp]: 
+    "~ neg ((number_of n)::int) ==> 0 <= x ==> 
+      natceiling (x + number_of n) = natceiling x + number_of n"
   apply (subst natceiling_add [THEN sym])
   apply simp_all
 done