src/HOL/ex/String.thy
changeset 4481 b595116eb3c4
parent 4253 901f690e3a58