src/HOL/String.thy
changeset 11364 01020b10c0a7
parent 10909 2bbb1797bbe2