src/HOL/OrderedGroup.thy
changeset 26071 046fe7ddfc4b
parent 26015 ad2756de580e
child 26480 544cef16045b
     1.1 --- a/src/HOL/OrderedGroup.thy	Fri Feb 15 14:20:51 2008 +0100
     1.2 +++ b/src/HOL/OrderedGroup.thy	Fri Feb 15 16:09:10 2008 +0100
     1.3 @@ -75,6 +75,9 @@
     1.4    assumes add_0_left [simp]: "0 + a = a"
     1.5      and add_0_right [simp]: "a + 0 = a"
     1.6  
     1.7 +lemma zero_reorient: "0 = x \<longleftrightarrow> x = 0"
     1.8 +  by (rule eq_commute)
     1.9 +
    1.10  class comm_monoid_add = zero + ab_semigroup_add +
    1.11    assumes add_0: "0 + a = a"
    1.12  begin
    1.13 @@ -88,6 +91,9 @@
    1.14    assumes mult_1_left [simp]: "1 * a  = a"
    1.15    assumes mult_1_right [simp]: "a * 1 = a"
    1.16  
    1.17 +lemma one_reorient: "1 = x \<longleftrightarrow> x = 1"
    1.18 +  by (rule eq_commute)
    1.19 +
    1.20  class comm_monoid_mult = one + ab_semigroup_mult +
    1.21    assumes mult_1: "1 * a = a"
    1.22  begin