src/HOL/String.thy
changeset 62378 85ed00c1fe7c
parent 62364 9209770bdcdf
child 62580 7011429f44f9