src/HOL/String.thy
changeset 60759 36d9f215c982
parent 60758 d8d85a8172b5
child 60801 7664e0916eec