Quot/QuotProd.thy
changeset 830 89d772dae4d4
parent 829 42b90994ac77
child 867 9e247b9505f0