src/HOL/String.thy
changeset 52264 cdba0c3cb4c2
parent 51717 9e7d1c139569
child 52365 95186e6e4bf4