src/Pure/sorts.ML
changeset 82432 314d6b215f90
parent 79447 57d29f537723