src/HOL/Tools/string_syntax.ML
changeset 35349 f9801fdeb789
parent 35262 9ea4445d2ccf
child 35363 09489d8ffece