src/Pure/sorts.ML
changeset 21966 edab0ecfbd7c
parent 21933 819ef284720b
child 22181 39104d1c43ca