1.1 --- a/src/HOL/Archimedean_Field.thy	Wed Jul 06 23:11:59 2011 +0200
     1.2 +++ b/src/HOL/Archimedean_Field.thy	Thu Jul 07 23:33:14 2011 +0200
     1.3 @@ -143,7 +143,7 @@
     1.4  
     1.5  definition
     1.6    floor :: "'a::archimedean_field \<Rightarrow> int" where
     1.7 -  "floor x = (THE z. of_int z \<le> x \<and> x < of_int (z + 1))"
     1.8 +  [code del]: "floor x = (THE z. of_int z \<le> x \<and> x < of_int (z + 1))"
     1.9  
    1.10  notation (xsymbols)
    1.11    floor  ("\<lfloor>_\<rfloor>")
    1.12 @@ -274,7 +274,7 @@
    1.13  
    1.14  definition
    1.15    ceiling :: "'a::archimedean_field \<Rightarrow> int" where
    1.16 -  "ceiling x = - floor (- x)"
    1.17 +  [code del]: "ceiling x = - floor (- x)"
    1.18  
    1.19  notation (xsymbols)
    1.20    ceiling  ("\<lceil>_\<rceil>")