src/HOL/String.thy
changeset 69768 7e4966eaf781
parent 69743 6a9a8ef5e4c6
child 69879 2731278dfff9