src/HOL/ex/String.thy
changeset 1072 0140ff702b23
parent 977 5d57287e5e1e
child 1376 92f83b9d17e1