src/Pure/name.ML
changeset 28091 50f2d6ba024c
parent 28075 a45ce1bae4e0
child 28108 1b08ed83b79e