changeset 27651 | 16a26996c30e |
parent 27468 | 0783dd1dc13d |
child 27682 | 25aceefd4786 |
27650:7a4baad05495 | 27651:16a26996c30e |
---|---|
529 |
529 |
530 instance .. |
530 instance .. |
531 |
531 |
532 end |
532 end |
533 |
533 |
534 instance star :: (Ring_and_Field.dvd) Ring_and_Field.dvd .. |
|
535 |
|
534 instantiation star :: (Divides.div) Divides.div |
536 instantiation star :: (Divides.div) Divides.div |
535 begin |
537 begin |
536 |
538 |
537 definition |
539 definition |
538 star_div_def: "(op div) \<equiv> *f2* (op div)" |
540 star_div_def: "(op div) \<equiv> *f2* (op div)" |