src/Pure/sorts.ML
changeset 57978 8f4a332500e4
parent 48272 db75b4005d9a
child 61262 7bd1eb4b056e
equal deleted inserted replaced
57977:113b43b84412 57978:8f4a332500e4