src/HOL/ex/StringEx.thy
changeset 11371 1d5d181b7e28
parent 11020 646c929b6293
child 11586 d8a7f6318457