src/Pure/defs.ML
changeset 82887 e5db7672d192
parent 74234 4f2bd13edce3