src/HOL/String.thy
changeset 54381 9c1f21365326
parent 54317 da932f511746
child 54594 a2d1522cdd54