src/Pure/General/long_name.ML
changeset 56202 0a11d17eeeff
parent 56162 ea6303e2261b
child 56800 b904ea8edd73
equal deleted inserted replaced
56201:dd2df97b379b 56202:0a11d17eeeff