Quot/QuotSum.thy
changeset 896 4e0b89d886ac
parent 829 42b90994ac77
child 924 5455b19ef138