src/HOL/String.thy
changeset 42707 42d607a9ae65
parent 42440 5e7a7343ab11
child 44278 1220ecb81e8f