src/HOL/String.ML
changeset 5126 01cbf154d926
parent 5121 5c1f89ae8aef
equal deleted inserted replaced
5125:463a0e9df5b5 5126:01cbf154d926