src/HOL/Real/RComplete.thy
changeset 27435 b3f8e9bdf9a7
parent 25162 ad4d5365d9d8
child 28091 50f2d6ba024c
--- a/src/HOL/Real/RComplete.thy	Tue Jul 01 21:30:12 2008 +0200
+++ b/src/HOL/Real/RComplete.thy	Wed Jul 02 07:11:57 2008 +0200
@@ -434,7 +434,7 @@
 
 definition
   floor :: "real => int" where
-  "floor r = (LEAST n::int. r < real (n+1))"
+  [code func del]: "floor r = (LEAST n::int. r < real (n+1))"
 
 definition
   ceiling :: "real => int" where