equal
deleted
inserted
replaced
211 lemmas Rep_simps = |
211 lemmas Rep_simps = |
212 Rep_inject_sym Rep_inverse Rep_Abs_mod Rep_mod Rep_Abs_0 Rep_Abs_1 |
212 Rep_inject_sym Rep_inverse Rep_Abs_mod Rep_mod Rep_Abs_0 Rep_Abs_1 |
213 |
213 |
214 lemma comm_ring_1: "OFCLASS('a, comm_ring_1_class)" |
214 lemma comm_ring_1: "OFCLASS('a, comm_ring_1_class)" |
215 apply (intro_classes, unfold definitions) |
215 apply (intro_classes, unfold definitions) |
216 apply (simp_all add: Rep_simps zmod_simps ring_simps) |
216 apply (simp_all add: Rep_simps zmod_simps field_simps) |
217 done |
217 done |
218 |
218 |
219 end |
219 end |
220 |
220 |
221 locale mod_ring = mod_type + |
221 locale mod_ring = mod_type + |