src/HOL/ex/StringEx.thy
changeset 11295 66925f23ac7f
parent 11020 646c929b6293
child 11586 d8a7f6318457