src/HOL/Rings.thy
changeset 35092 cfe605c54e50
parent 35083 3246e66b0874
child 35097 4554bb2abfa3
     1.1 --- a/src/HOL/Rings.thy	Wed Feb 10 14:12:02 2010 +0100
     1.2 +++ b/src/HOL/Rings.thy	Wed Feb 10 14:12:04 2010 +0100
     1.3 @@ -782,15 +782,6 @@
     1.4  
     1.5  end
     1.6  
     1.7 -class abs_if = minus + uminus + ord + zero + abs +
     1.8 -  assumes abs_if: "\<bar>a\<bar> = (if a < 0 then - a else a)"
     1.9 -
    1.10 -class sgn_if = minus + uminus + zero + one + ord + sgn +
    1.11 -  assumes sgn_if: "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
    1.12 -
    1.13 -lemma (in sgn_if) sgn0[simp]: "sgn 0 = 0"
    1.14 -by(simp add:sgn_if)
    1.15 -
    1.16  class linordered_ring = ring + linordered_semiring + linordered_ab_group_add + abs_if
    1.17  begin
    1.18