src/HOL/String.thy
changeset 60864 20cfa048fe7c
parent 60801 7664e0916eec
child 61032 b57df8eecad6