src/HOL/ex/StringEx.ML
changeset 7843 077d305615df
parent 5278 a903b66822e2
child 8035 84c5ce912b43