src/Pure/General/long_name.ML
changeset 56720 e1317a26f8c0
parent 56162 ea6303e2261b
child 56800 b904ea8edd73