src/Pure/defs.ML
changeset 80701 39cd50407f79
parent 74234 4f2bd13edce3
equal deleted inserted replaced
80700:f6c6d0988fba 80701:39cd50407f79