src/HOL/String.thy
changeset 44256 c478cd500dc4
parent 42440 5e7a7343ab11
child 44278 1220ecb81e8f