src/HOL/String.thy
changeset 64561 a7664ca9ffc5
parent 63950 cdc1e59aa513
child 64630 96015aecfeba