src/Pure/term_ord.ML
changeset 30988 b53800e3ee47
parent 29269 5c25a2012975
child 31971 8c1b845ed105
equal deleted inserted replaced
30987:2bbc22bd6a95 30988:b53800e3ee47