quotient_def.ML
changeset 583 7414f6cb5398
parent 573 14682786c356