src/Pure/defs.ML
changeset 17740 fc385ce6187d
parent 17712 46c2091e5187
child 17803 e235a57651a1