src/Pure/term_ord.ML
changeset 78010 6c2494750a4e
parent 77883 2cd00c4054ab
child 79096 48187f1a615e