src/HOL/ex/StringEx.ML
changeset 7025 afbd8241797b
parent 5278 a903b66822e2
child 8035 84c5ce912b43