equal
deleted
inserted
replaced
180 |
180 |
181 |
181 |
182 subsection \<open>Ring class instances\<close> |
182 subsection \<open>Ring class instances\<close> |
183 |
183 |
184 text \<open> |
184 text \<open> |
185 Unfortunately @{text ring_1} instance is not possible for |
185 Unfortunately \<open>ring_1\<close> instance is not possible for |
186 @{typ num1}, since 0 and 1 are not distinct. |
186 @{typ num1}, since 0 and 1 are not distinct. |
187 \<close> |
187 \<close> |
188 |
188 |
189 instantiation num1 :: "{comm_ring,comm_monoid_mult,numeral}" |
189 instantiation num1 :: "{comm_ring,comm_monoid_mult,numeral}" |
190 begin |
190 begin |