src/HOL/ex/IntRing.thy
changeset 5601 b6456ccd9e3e
parent 5078 7b5ea59c0275
child 6921 78a2ce8fb8df
equal deleted inserted replaced
5600:34b3366b83ac 5601:b6456ccd9e3e
     8 *)
     8 *)
     9 
     9 
    10 IntRing = IntRingDefs + Lagrange +
    10 IntRing = IntRingDefs + Lagrange +
    11 
    11 
    12 instance int :: add_semigroup (zadd_assoc)
    12 instance int :: add_semigroup (zadd_assoc)
    13 instance int :: add_monoid (zero_int_def,zadd_0,zadd_0_right)
    13 instance int :: add_monoid (zero_int_def,zadd_nat0,zadd_nat0_right)
    14 instance int :: add_group (left_inv_int,minus_inv_int)
    14 instance int :: add_group (left_inv_int,minus_inv_int)
    15 instance int :: add_agroup (zadd_commute)
    15 instance int :: add_agroup (zadd_commute)
    16 instance int :: ring (zmult_assoc,zadd_zmult_distrib2,zadd_zmult_distrib)
    16 instance int :: ring (zmult_assoc,zadd_zmult_distrib2,zadd_zmult_distrib)
    17 instance int :: cring (zmult_commute)
    17 instance int :: cring (zmult_commute)
    18 
    18