src/HOL/ex/IntRing.thy
changeset 11868 56db9f3a6b3e
parent 11701 3d51fbf81c17
equal deleted inserted replaced
11867:76401b2ee871 11868:56db9f3a6b3e
     8 *)
     8 *)
     9 
     9 
    10 IntRing = Ring + Lagrange +
    10 IntRing = Ring + 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_int0,zadd_int0_right)
    13 instance int :: add_monoid (zadd_0,zadd_0_right)
    14 instance int :: add_group {|Auto_tac|}
    14 instance int :: add_group {|Auto_tac|}
    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