src/HOL/Quot/PER.ML
changeset 9477 9506127f6fbb
parent 6162 484adda70b65