Quot/quotient_def.ML
changeset 857 0ce025c02ef3
parent 856 433f7c17255f
child 858 bb012513fb39