src/HOL/String.thy
changeset 11371 1d5d181b7e28
parent 10909 2bbb1797bbe2