Quot/quotient_def.ML
changeset 861 e3d17c4b3eca
parent 858 bb012513fb39
child 862 09ec51d50fc6