src/HOL/String.thy
changeset 11511 ec89f5cff390
parent 10909 2bbb1797bbe2