src/Pure/term_ord.ML
changeset 78924 0481c84f6919
parent 77883 2cd00c4054ab
child 79096 48187f1a615e