src/HOL/SupInf.thy
changeset 37765 26bdfb7b680b
parent 36777 be5461582d0f
child 37887 2ae085b07f2f
     1.1 --- a/src/HOL/SupInf.thy	Mon Jul 12 08:58:12 2010 +0200
     1.2 +++ b/src/HOL/SupInf.thy	Mon Jul 12 08:58:13 2010 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  instantiation real :: Sup 
     1.5  begin
     1.6  definition
     1.7 -  Sup_real_def [code del]: "Sup X == (LEAST z::real. \<forall>x\<in>X. x\<le>z)"
     1.8 +  Sup_real_def: "Sup X == (LEAST z::real. \<forall>x\<in>X. x\<le>z)"
     1.9  
    1.10  instance ..
    1.11  end
    1.12 @@ -17,7 +17,7 @@
    1.13  instantiation real :: Inf 
    1.14  begin
    1.15  definition
    1.16 -  Inf_real_def [code del]: "Inf (X::real set) == - (Sup (uminus ` X))"
    1.17 +  Inf_real_def: "Inf (X::real set) == - (Sup (uminus ` X))"
    1.18  
    1.19  instance ..
    1.20  end