src/Pure/name.ML
changeset 23597 ab67175ca8a5
parent 21565 bd28361f4c5b
child 24849 193a10e6bf90
equal deleted inserted replaced
23596:f8381a95c49c 23597:ab67175ca8a5