src/HOL/String.thy
changeset 62553 d2e0d626fb96
parent 62364 9209770bdcdf
child 62580 7011429f44f9