src/HOL/Quot/PER0.ML
changeset 7360 7d3136b9af08
parent 5858 beddc19c107a