src/HOL/String.thy
changeset 11008 f7333f055ef6
parent 10909 2bbb1797bbe2