src/Pure/config.ML
changeset 40650 d40b347d5b0b
parent 40291 012ed4426fda
child 47814 53668571d300
equal deleted inserted replaced
40649:dc1b5aa908ff 40650:d40b347d5b0b