src/Pure/sorts.ML
changeset 72574 d892f6d66402
parent 71526 abe723ff3f7f
child 74232 1091880266e5