src/Pure/pure_setup.ML
changeset 40650 d40b347d5b0b
parent 38470 484e483eb606
child 40741 17d6293a1e26
equal deleted inserted replaced
40649:dc1b5aa908ff 40650:d40b347d5b0b