src/Pure/term_ord.ML
changeset 79578 4c4d71b00001
parent 79096 48187f1a615e