src/Pure/General/string.ML
changeset 78748 ca486ee0e4c5
parent 77847 3bb6468d202e