src/HOL/ex/StringEx.ML
changeset 6392 e2ecfd8622ae
parent 5278 a903b66822e2
child 8035 84c5ce912b43