| changeset 23686 | 9d5671f61b31 |
| parent 23132 | ae52b82dc5d8 |
| child 23881 | 851c74f1bb69 |
| 23685:1b0f4071946c | 23686:9d5671f61b31 |
|---|---|
206 end_import; |
206 end_import; |
207 |
207 |
208 import_theory divides; |
208 import_theory divides; |
209 |
209 |
210 const_maps |
210 const_maps |
211 divides > "Divides.dvd" :: "[nat,nat]=>bool"; |
211 divides > Divides.times_class.dvd :: "[nat,nat]=>bool"; |
212 |
212 |
213 end_import; |
213 end_import; |
214 |
214 |
215 import_theory prime; |
215 import_theory prime; |
216 end_import; |
216 end_import; |