src/HOL/Quot/PER.ML
changeset 3362 0b268cff9344
parent 2904 fc10751254aa
child 3457 a8ab7c64817c