src/Pure/term.ML
changeset 435 ca5356bd315a
parent 375 d7ae7ac22d48
child 728 9a973c3ba350
equal deleted inserted replaced
434:89d45187f04d 435:ca5356bd315a