src/HOL/Algebra/UnivPoly.thy
changeset 44821 a92f65e174cf
parent 44655 fe0365331566
child 44890 22f665a2e91c
     1.1 --- a/src/HOL/Algebra/UnivPoly.thy	Wed Sep 07 14:58:40 2011 +0200
     1.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Wed Sep 07 09:02:58 2011 -0700
     1.3 @@ -1818,7 +1818,7 @@
     1.4  
     1.5  lemma INTEG_cring: "cring INTEG"
     1.6    by (unfold INTEG_def) (auto intro!: cringI abelian_groupI comm_monoidI
     1.7 -    zadd_zminus_inverse2 zadd_zmult_distrib)
     1.8 +    left_minus left_distrib)
     1.9  
    1.10  lemma INTEG_id_eval:
    1.11    "UP_pre_univ_prop INTEG INTEG id"