src/HOL/String.thy
changeset 54643 57aefb80b639
parent 54317 da932f511746
child 54594 a2d1522cdd54