src/Pure/General/string.ML
changeset 80161 fd5ed5e63a29
parent 77847 3bb6468d202e