src/HOL/String.thy
changeset 11003 ee0838d89deb
parent 10909 2bbb1797bbe2