src/HOL/Quot/PER0.ML
changeset 8857 7ec405405dd7
parent 5858 beddc19c107a