src/Pure/defs.ML
changeset 57978 8f4a332500e4
parent 57520 3ad1b289f21b
child 59050 376446e98951