src/Pure/General/string.ML
changeset 82282 919eb0e67930
parent 77847 3bb6468d202e