src/HOL/String.thy
changeset 51372 d315e9a9ee72
parent 51160 599ff65b85e2
child 51717 9e7d1c139569