src/Pure/defs.ML
changeset 57907 7fc36b4c7cce
parent 57520 3ad1b289f21b
child 59050 376446e98951