# HG changeset patch
# User nipkow
# Date 1310120326 -7200
# Node ID 4068e95f1e43ad9d2dab974fcad8b628518cc11c
# Parent  47b0be18ccbea838adc69c416049f0a3eff94b9e# Parent  8e421a529a487ad1e34a8c5a12c842e1d5715c99
merged

diff -r 8e421a529a48 -r 4068e95f1e43 src/HOL/Archimedean_Field.thy
--- a/src/HOL/Archimedean_Field.thy	Thu Jul 07 21:53:53 2011 +0200
+++ b/src/HOL/Archimedean_Field.thy	Fri Jul 08 12:18:46 2011 +0200
@@ -143,7 +143,7 @@
 
 definition
   floor :: "'a::archimedean_field \<Rightarrow> int" where
-  "floor x = (THE z. of_int z \<le> x \<and> x < of_int (z + 1))"
+  [code del]: "floor x = (THE z. of_int z \<le> x \<and> x < of_int (z + 1))"
 
 notation (xsymbols)
   floor  ("\<lfloor>_\<rfloor>")
@@ -274,7 +274,7 @@
 
 definition
   ceiling :: "'a::archimedean_field \<Rightarrow> int" where
-  "ceiling x = - floor (- x)"
+  [code del]: "ceiling x = - floor (- x)"
 
 notation (xsymbols)
   ceiling  ("\<lceil>_\<rceil>")