src/HOL/Real/RealDef.thy
changeset 26513 6f306c8c2c54
parent 25965 05df64f786a4
child 26732 6ea9de67e576
     1.1 --- a/src/HOL/Real/RealDef.thy	Wed Apr 02 15:58:31 2008 +0200
     1.2 +++ b/src/HOL/Real/RealDef.thy	Wed Apr 02 15:58:32 2008 +0200
     1.3 @@ -978,10 +978,17 @@
     1.4    "1 = Ratreal 1\<^sub>N" by simp
     1.5  declare one_real_code [symmetric, code post]
     1.6  
     1.7 -instance real :: eq ..
     1.8 +instantiation real :: eq
     1.9 +begin
    1.10 +
    1.11 +definition "eq (x\<Colon>real) y \<longleftrightarrow> x = y"
    1.12 +
    1.13 +instance by default (simp add: eq_real_def)
    1.14  
    1.15  lemma real_eq_code [code]: "Ratreal x = Ratreal y \<longleftrightarrow> normNum x = normNum y"
    1.16 -  unfolding Ratreal_def INum_normNum_iff ..
    1.17 +  unfolding Ratreal_def INum_normNum_iff eq ..
    1.18 +
    1.19 +end
    1.20  
    1.21  lemma real_less_eq_code [code]: "Ratreal x \<le> Ratreal y \<longleftrightarrow> normNum x \<le>\<^sub>N normNum y"
    1.22  proof -