src/Pure/General/name_space.ML
changeset 40650 d40b347d5b0b
parent 35679 da87ffdcf7ea
child 41254 78c3e472bb35
equal deleted inserted replaced
40649:dc1b5aa908ff 40650:d40b347d5b0b