src/Pure/name.ML
changeset 22569 e5d7d9de7d85
parent 21565 bd28361f4c5b
child 24849 193a10e6bf90
equal deleted inserted replaced
22568:ed7aa5a350ef 22569:e5d7d9de7d85