src/HOL/Quot/PER.ML
changeset 5330 8c9fadda81f4
parent 5069 3ea049f7979d
child 5858 beddc19c107a