src/HOL/Archimedean_Field.thy
changeset 37765 26bdfb7b680b
parent 35028 108662d50512
child 41959 b460124855b8
     1.1 --- a/src/HOL/Archimedean_Field.thy	Mon Jul 12 08:58:12 2010 +0200
     1.2 +++ b/src/HOL/Archimedean_Field.thy	Mon Jul 12 08:58:13 2010 +0200
     1.3 @@ -143,7 +143,7 @@
     1.4  
     1.5  definition
     1.6    floor :: "'a::archimedean_field \<Rightarrow> int" where
     1.7 -  [code del]: "floor x = (THE z. of_int z \<le> x \<and> x < of_int (z + 1))"
     1.8 +  "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 -  [code del]: "ceiling x = - floor (- x)"
    1.17 +  "ceiling x = - floor (- x)"
    1.18  
    1.19  notation (xsymbols)
    1.20    ceiling  ("\<lceil>_\<rceil>")