| changeset 532 | 53984a386999 |
| parent 529 | 6348c2a57ec2 |
| child 700 | 91b079db7380 |
| 531:3feed4dbfa45 | 532:53984a386999 |
|---|---|
46 |
46 |
47 - Integrate RSP/PRS lemmas in QuotList with the ones from IntEx etc. |
47 - Integrate RSP/PRS lemmas in QuotList with the ones from IntEx etc. |
48 |
48 |
49 - Check all the places where we do "handle _" |
49 - Check all the places where we do "handle _" |
50 |
50 |
51 - We shouldn't use the command 'quotient' as this shadows Larry's quotient. |
|
52 Call it 'quotient_type' |