src/HOL/String.thy
changeset 68048 0b4fb9fd91b1
parent 68033 ad4b8b6892c3
child 68224 1f7308050349