src/Pure/sorts.ML
changeset 74215 7515abfe18cf
parent 71526 abe723ff3f7f
child 74232 1091880266e5