src/HOL/ex/IntRing.thy
changeset 8936 a1c426541757
parent 6921 78a2ce8fb8df
child 11701 3d51fbf81c17
equal deleted inserted replaced
8935:548901d05a0e 8936:a1c426541757
     5 
     5 
     6 The integers form a commutative ring.
     6 The integers form a commutative ring.
     7 With an application of Lagrange's lemma.
     7 With an application of Lagrange's lemma.
     8 *)
     8 *)
     9 
     9 
    10 IntRing = IntRingDefs + 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 (IntDef.Zero_def,zadd_int0,zadd_int0_right)
    14 instance int :: add_group (left_inv_int,minus_inv_int)
    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 
    19 end
    19 end