src/HOL/ex/StringEx.thy
changeset 19915 b08e26fb247e
parent 17388 495c799df31d