src/HOL/String.thy
changeset 52593 aedf7b01c6e4
parent 52435 6646bb548c6b
child 52910 7bfe0df532a9