src/Pure/General/string.ML
changeset 79139 359abf434d70
parent 77847 3bb6468d202e