src/Pure/defs.ML
changeset 53010 ec5e6f69bd65
parent 42389 b2c6033fc7e4
child 55544 cf1baba89a27