src/HOL/Quot/PER0.ML
changeset 5253 82a5ca6290aa
parent 5069 3ea049f7979d
child 5858 beddc19c107a