src/HOL/String.ML
changeset 5154 40fd46f3d3a1
parent 5121 5c1f89ae8aef