src/HOL/Quot/PER0.ML
changeset 3362 0b268cff9344
parent 3058 9d6526cacc3c
child 3457 a8ab7c64817c