src/Pure/defs.ML
changeset 80246 245dd5f82462
parent 74234 4f2bd13edce3