src/HOL/ex/String.thy
changeset 5078 7b5ea59c0275
parent 4253 901f690e3a58