src/Pure/context.ML
changeset 8896 c80aba8c1d5e
parent 8801 9d01c9a26134
child 9586 f6669dead969
equal deleted inserted replaced
8895:2913a54e64cf 8896:c80aba8c1d5e