# HG changeset patch
# User obua
# Date 1196870090 -3600
# Node ID 4f8d7ac83c0be255ab0f1b6f7c5111a09dd74305
# Parent  21cd20c1ce9808fb1228a45e90f223c8393a3872
instance int,real :: lordered_ring

diff -r 21cd20c1ce98 -r 4f8d7ac83c0b src/HOL/Real/RealDef.thy
--- a/src/HOL/Real/RealDef.thy	Wed Dec 05 14:36:58 2007 +0100
+++ b/src/HOL/Real/RealDef.thy	Wed Dec 05 16:54:50 2007 +0100
@@ -993,6 +993,20 @@
 lemma real_div_code [code]: "Ratreal x / Ratreal y = Ratreal (x \<div>\<^sub>N y)"
   unfolding Ratreal_def by simp
 
+instance int :: lordered_ring
+proof  
+  fix a::int
+  show "abs a = sup a (- a)"
+    by (auto simp add: zabs_def sup_int_def)
+qed
+
+instance real :: lordered_ring
+proof
+  fix a::real
+  show "abs a = sup a (-a)"
+    by (auto simp add: real_abs_def sup_real_def)
+qed
+
 text {* Setup for SML code generator *}
 
 types_code