src/HOL/Real/RComplete.thy
changeset 28562 4e74209f113e
parent 28091 50f2d6ba024c
--- a/src/HOL/Real/RComplete.thy	Fri Oct 10 06:45:50 2008 +0200
+++ b/src/HOL/Real/RComplete.thy	Fri Oct 10 06:45:53 2008 +0200
@@ -488,7 +488,7 @@
 
 definition
   floor :: "real => int" where
-  [code func del]: "floor r = (LEAST n::int. r < real (n+1))"
+  [code del]: "floor r = (LEAST n::int. r < real (n+1))"
 
 definition
   ceiling :: "real => int" where