src/Pure/term_ord.ML
changeset 76166 dbafa8d688fb
parent 74270 ad2899cdd528
child 77723 b761c91c2447
equal deleted inserted replaced
76165:cf469736000c 76166:dbafa8d688fb