src/HOL/Quot/PER.ML
changeset 7584 5be4bb8e4e3f
parent 6162 484adda70b65