src/HOL/String.thy
changeset 11557 66b62cbeaab3
parent 10909 2bbb1797bbe2