src/HOL/String.thy
changeset 52183 667961fa6a60
parent 51717 9e7d1c139569
child 52365 95186e6e4bf4