src/HOL/Real/RealDef.thy
changeset 25546 4f8d7ac83c0b
parent 25502 9200b36280c0
child 25571 c9e39eafc7a0
     1.1 --- a/src/HOL/Real/RealDef.thy	Wed Dec 05 14:36:58 2007 +0100
     1.2 +++ b/src/HOL/Real/RealDef.thy	Wed Dec 05 16:54:50 2007 +0100
     1.3 @@ -993,6 +993,20 @@
     1.4  lemma real_div_code [code]: "Ratreal x / Ratreal y = Ratreal (x \<div>\<^sub>N y)"
     1.5    unfolding Ratreal_def by simp
     1.6  
     1.7 +instance int :: lordered_ring
     1.8 +proof  
     1.9 +  fix a::int
    1.10 +  show "abs a = sup a (- a)"
    1.11 +    by (auto simp add: zabs_def sup_int_def)
    1.12 +qed
    1.13 +
    1.14 +instance real :: lordered_ring
    1.15 +proof
    1.16 +  fix a::real
    1.17 +  show "abs a = sup a (-a)"
    1.18 +    by (auto simp add: real_abs_def sup_real_def)
    1.19 +qed
    1.20 +
    1.21  text {* Setup for SML code generator *}
    1.22  
    1.23  types_code