src/HOL/String.thy
changeset 31409 d8537ba165b5
parent 31205 98370b26c2ce
child 31484 cabcb95fde29