src/HOL/Real/RComplete.thy
changeset 21404 eb85850d3eb7
parent 21210 c17fd2df4e9e
child 22998 97e1f9c2cc46
--- a/src/HOL/Real/RComplete.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Real/RComplete.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -432,18 +432,19 @@
 subsection{*Floor and Ceiling Functions from the Reals to the Integers*}
 
 definition
-  floor :: "real => int"
+  floor :: "real => int" where
   "floor r = (LEAST n::int. r < real (n+1))"
 
-  ceiling :: "real => int"
+definition
+  ceiling :: "real => int" where
   "ceiling r = - floor (- r)"
 
 notation (xsymbols)
-  floor  ("\<lfloor>_\<rfloor>")
+  floor  ("\<lfloor>_\<rfloor>") and
   ceiling  ("\<lceil>_\<rceil>")
 
 notation (HTML output)
-  floor  ("\<lfloor>_\<rfloor>")
+  floor  ("\<lfloor>_\<rfloor>") and
   ceiling  ("\<lceil>_\<rceil>")
 
 
@@ -933,9 +934,11 @@
 subsection {* Versions for the natural numbers *}
 
 definition
-  natfloor :: "real => nat"
+  natfloor :: "real => nat" where
   "natfloor x = nat(floor x)"
-  natceiling :: "real => nat"
+
+definition
+  natceiling :: "real => nat" where
   "natceiling x = nat(ceiling x)"
 
 lemma natfloor_zero [simp]: "natfloor 0 = 0"