src/HOL/Quot/PER0.ML
changeset 5971 c5a7a7685826
parent 5858 beddc19c107a