src/Pure/sorts.ML
changeset 80512 6a58d706cfb2
parent 79447 57d29f537723