equal
deleted
inserted
replaced
78 class comm_monoid_mult = one + ab_semigroup_mult + |
78 class comm_monoid_mult = one + ab_semigroup_mult + |
79 assumes mult_1: "1 * a = a" |
79 assumes mult_1: "1 * a = a" |
80 begin |
80 begin |
81 |
81 |
82 subclass monoid_mult |
82 subclass monoid_mult |
83 by unfold_locales (insert mult_1, simp_all add: mult_commute) |
83 by unfold_locales (insert mult_1, simp_all add: mult_commute) |
84 |
84 |
85 end |
85 end |
86 |
86 |
87 class cancel_semigroup_add = semigroup_add + |
87 class cancel_semigroup_add = semigroup_add + |
88 assumes add_left_imp_eq: "a + b = a + c \<Longrightarrow> b = c" |
88 assumes add_left_imp_eq: "a + b = a + c \<Longrightarrow> b = c" |