src/HOL/String.thy
changeset 60976 0a8c719d8c1f
parent 60801 7664e0916eec
child 61032 b57df8eecad6