src/HOL/ex/StringEx.ML
changeset 11582 f666c1e4133d
parent 8035 84c5ce912b43