# HG changeset patch
# User haftmann
# Date 1240420162 -7200
# Node ID 541bfff659af681b41b750c7db0a625a991027b1
# Parent  fec1a04b7220c440bf56f6e366d08360a79634ff
more localisation

diff -r fec1a04b7220 -r 541bfff659af src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Wed Apr 22 19:09:21 2009 +0200
+++ b/src/HOL/Ring_and_Field.thy	Wed Apr 22 19:09:22 2009 +0200
@@ -2226,15 +2226,21 @@
 qed
 qed
 
-instance ordered_idom \<subseteq> pordered_ring_abs
-by default (auto simp add: abs_if not_less
-  equal_neg_zero neg_equal_zero mult_less_0_iff)
-
-lemma abs_mult: "abs (a * b) = abs a * abs (b::'a::ordered_idom)" 
-by (simp add: abs_eq_mult linorder_linear)
-
-lemma abs_mult_self: "abs a * abs a = a * (a::'a::ordered_idom)"
-by (simp add: abs_if) 
+context ordered_idom
+begin
+
+subclass pordered_ring_abs proof
+qed (auto simp add: abs_if not_less equal_neg_zero neg_equal_zero mult_less_0_iff)
+
+lemma abs_mult:
+  "abs (a * b) = abs a * abs b" 
+  by (rule abs_eq_mult) auto
+
+lemma abs_mult_self:
+  "abs a * abs a = a * a"
+  by (simp add: abs_if) 
+
+end
 
 lemma nonzero_abs_inverse:
      "a \<noteq> 0 ==> abs (inverse (a::'a::ordered_field)) = inverse (abs a)"