src/Pure/context.ML
changeset 74330 d882abae3379
parent 74234 4f2bd13edce3
child 74461 8e9f38240c05
equal deleted inserted replaced
74327:9dca3df78b6a 74330:d882abae3379