src/Pure/sorts.ML
changeset 10120 0f315aeee16e
parent 9281 a48818595670
child 14782 d6ce35a1c386
equal deleted inserted replaced
10119:20c9590bb5f5 10120:0f315aeee16e