src/Pure/defs.ML
changeset 19420 bd5c0adec2b1
parent 19339 59f08f67ed3f
child 19482 9f11af8f7ef9