Quot/quotient_def.ML
changeset 761 e2ac18492c68
parent 760 c1989de100b4
child 762 baac4639ecef