src/HOL/String.thy
changeset 42230 594480d25aaa
parent 42163 392fd6c4669c
child 42411 ff997038e8eb