src/HOL/String.thy
changeset 64865 778c64c17363
parent 64630 96015aecfeba
child 64994 6e4c05e8edbb