src/HOL/ex/String.thy
changeset 4375 ef2a7b589004
parent 4253 901f690e3a58