src/Pure/sorts.ML
changeset 73746 b2d47981c8dc
parent 71526 abe723ff3f7f
child 74232 1091880266e5