changeset 529 | 6348c2a57ec2 |
parent 527 | 9b1ad366827f |
child 700 | 91b079db7380 |
528:f51e2b3e3149 | 529:6348c2a57ec2 |
---|---|
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' |