src/HOL/Algebra/UnivPoly.thy
changeset 13975 c8e9a89883ce
parent 13949 0ce528cd6f19
child 14399 dc677b35e54f
     1.1 --- a/src/HOL/Algebra/UnivPoly.thy	Wed May 07 17:46:04 2003 +0200
     1.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Wed May 07 22:07:33 2003 +0200
     1.3 @@ -1515,6 +1515,15 @@
     1.4    by (fast intro: ring_hom_UP_cring.intro ring_hom_cring_axioms.intro
     1.5      cring.axioms prems)
     1.6  
     1.7 +constdefs
     1.8 +  INTEG :: "int ring"
     1.9 +  "INTEG == (| carrier = UNIV, mult = op *, one = 1, zero = 0, add = op + |)"
    1.10 +
    1.11 +lemma cring_INTEG:
    1.12 +  "cring INTEG"
    1.13 +  by (unfold INTEG_def) (auto intro!: cringI abelian_groupI comm_monoidI
    1.14 +    zadd_zminus_inverse2 zadd_zmult_distrib)
    1.15 +
    1.16  lemma INTEG_id:
    1.17    "ring_hom_UP_cring INTEG INTEG id"
    1.18    by (fast intro: ring_hom_UP_cringI cring_INTEG id_ring_hom)