equal
deleted
inserted
replaced
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 (IntDef.Zero_def,zadd_int0,zadd_int0_right) |
13 instance int :: add_monoid (Zero_int_def,zadd_int0,zadd_int0_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 |