src/HOL/ex/String.thy
changeset 1228 7d6b0241afab
parent 977 5d57287e5e1e
child 1376 92f83b9d17e1