src/HOL/String.thy
changeset 54574 d04e74341d43
parent 54317 da932f511746
child 54594 a2d1522cdd54