src/Pure/sorts.ML
changeset 30126 332e739b6b0e
parent 30065 c9a1e0f7621b
child 30242 aea5d7fa7ef5
equal deleted inserted replaced
30124:b956bf0dc87c 30126:332e739b6b0e