src/HOL/ex/StringEx.ML
changeset 6392 e2ecfd8622ae
parent 5278 a903b66822e2
child 8035 84c5ce912b43
equal deleted inserted replaced
6391:0da748358eff 6392:e2ecfd8622ae