src/Pure/defs.ML
changeset 57915 448325de6e4f
parent 57520 3ad1b289f21b
child 59050 376446e98951