src/HOL/ex/String.ML
changeset 5078 7b5ea59c0275
parent 5069 3ea049f7979d