src/HOL/ex/IntRing.thy
changeset 6921 78a2ce8fb8df
parent 5601 b6456ccd9e3e
child 8936 a1c426541757
equal deleted inserted replaced
6920:c912740c3545 6921:78a2ce8fb8df
     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_nat0,zadd_nat0_right)
    13 instance int :: add_monoid (zero_int_def,zadd_int0,zadd_int0_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