src/HOL/String.thy
changeset 42224 578a51fae383
parent 42163 392fd6c4669c
child 42411 ff997038e8eb