src/Pure/defs.ML
changeset 16665 b75568de32c6
parent 16384 90c51c932154
child 16743 21dbff595bf6