src/HOL/Algebra/UnivPoly.thy
changeset 49962 a8cc904a6820
parent 44890 22f665a2e91c
child 54863 82acc20ded73
     1.1 --- a/src/HOL/Algebra/UnivPoly.thy	Fri Oct 19 10:46:42 2012 +0200
     1.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Fri Oct 19 15:12:52 2012 +0200
     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 -    left_minus left_distrib)
     1.8 +    left_minus distrib_right)
     1.9  
    1.10  lemma INTEG_id_eval:
    1.11    "UP_pre_univ_prop INTEG INTEG id"