src/HOL/Real/RealDef.thy
changeset 25965 05df64f786a4
parent 25885 6fbc3f54f819
child 26513 6f306c8c2c54
     1.1 --- a/src/HOL/Real/RealDef.thy	Fri Jan 25 14:53:58 2008 +0100
     1.2 +++ b/src/HOL/Real/RealDef.thy	Fri Jan 25 14:54:41 2008 +0100
     1.3 @@ -852,14 +852,14 @@
     1.4  begin
     1.5  
     1.6  definition
     1.7 -  real_number_of_def: "number_of w = real_of_int w"
     1.8 +  real_number_of_def [code func del]: "number_of w = real_of_int w"
     1.9  
    1.10  instance
    1.11    by intro_classes (simp add: real_number_of_def)
    1.12  
    1.13  end
    1.14  
    1.15 -lemma [code, code unfold]:
    1.16 +lemma [code unfold, symmetric, code post]:
    1.17    "number_of k = real_of_int (number_of k)"
    1.18    unfolding number_of_is_id real_number_of_def ..
    1.19  
    1.20 @@ -972,9 +972,11 @@
    1.21  
    1.22  lemma zero_real_code [code, code unfold]:
    1.23    "0 = Ratreal 0\<^sub>N" by simp
    1.24 +declare zero_real_code [symmetric, code post]
    1.25  
    1.26  lemma one_real_code [code, code unfold]:
    1.27    "1 = Ratreal 1\<^sub>N" by simp
    1.28 +declare one_real_code [symmetric, code post]
    1.29  
    1.30  instance real :: eq ..
    1.31  
    1.32 @@ -1015,13 +1017,6 @@
    1.33  lemma real_div_code [code]: "Ratreal x / Ratreal y = Ratreal (x \<div>\<^sub>N y)"
    1.34    unfolding Ratreal_def by simp
    1.35  
    1.36 -instance int :: lordered_ring
    1.37 -proof  
    1.38 -  fix a::int
    1.39 -  show "abs a = sup a (- a)"
    1.40 -    by (auto simp add: zabs_def sup_int_def)
    1.41 -qed
    1.42 -
    1.43  instance real :: lordered_ring
    1.44  proof
    1.45    fix a::real