src/Pure/General/long_name.ML
changeset 56754 21662be93f4c
parent 56162 ea6303e2261b
child 56800 b904ea8edd73