src/HOL/String.thy
changeset 52369 0b395800fdf0
parent 52365 95186e6e4bf4
child 52435 6646bb548c6b