src/HOL/String.thy
changeset 69855 60b924cda764
parent 69743 6a9a8ef5e4c6
child 69879 2731278dfff9