Quot/quotient_info.ML
changeset 785 bf6861ee3b90
parent 784 da75568e7f12
child 786 d6407afb913c