src/Pure/defs.ML
changeset 58839 ccda99401bc8
parent 57520 3ad1b289f21b
child 59050 376446e98951