--- a/src/HOL/Rings.thy Wed Feb 10 14:12:02 2010 +0100
+++ b/src/HOL/Rings.thy Wed Feb 10 14:12:04 2010 +0100
@@ -782,15 +782,6 @@
end
-class abs_if = minus + uminus + ord + zero + abs +
- assumes abs_if: "\<bar>a\<bar> = (if a < 0 then - a else a)"
-
-class sgn_if = minus + uminus + zero + one + ord + sgn +
- assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
-
-lemma (in sgn_if) sgn0[simp]: "sgn 0 = 0"
-by(simp add:sgn_if)
-
class linordered_ring = ring + linordered_semiring + linordered_ab_group_add + abs_if
begin