src/HOL/Tools/string_syntax.ML
changeset 53470 fe80dd7cd543
parent 52143 36ffe23b25f8
child 55015 e33c5bd729ff
equal deleted inserted replaced
53469:3356a148b783 53470:fe80dd7cd543