src/HOL/String.thy
changeset 58299 30ab8289f0e1
parent 58152 6fe60a9a5bad
child 58310 91ea607a34d8