src/Pure/sorts.ML
changeset 9927 7a9652294fe0
parent 9281 a48818595670
child 14782 d6ce35a1c386