src/HOL/Semiring_Normalization.thy
changeset 37946 be3c0df7bb90
parent 36873 112e613e8d0b
child 47108 2a1953f0d20d
equal deleted inserted replaced
37945:32f9b7a70fc0 37946:be3c0df7bb90
    34   "b = b + a \<longleftrightarrow> a = 0"
    34   "b = b + a \<longleftrightarrow> a = 0"
    35   using add_imp_eq [of b a 0] by auto
    35   using add_imp_eq [of b a 0] by auto
    36 
    36 
    37 end
    37 end
    38 
    38 
    39 sublocale idom < comm_semiring_1_cancel_crossproduct
    39 subclass (in idom) comm_semiring_1_cancel_crossproduct
    40 proof
    40 proof
    41   fix w x y z
    41   fix w x y z
    42   show "w * y + x * z = w * z + x * y \<longleftrightarrow> w = x \<or> y = z"
    42   show "w * y + x * z = w * z + x * y \<longleftrightarrow> w = x \<or> y = z"
    43   proof
    43   proof
    44     assume "w * y + x * z = w * z + x * y"
    44     assume "w * y + x * z = w * z + x * y"