src/HOL/String.thy
changeset 54492 6fae4ecd4ab3
parent 54317 da932f511746
child 54594 a2d1522cdd54