src/HOL/Quot/NPAIR.ML
changeset 8488 58e37d59c146
parent 5858 beddc19c107a