src/HOL/Tools/string_syntax.ML
changeset 80987 e7a926b5b5be
parent 80795 5e38e8b34eb3
child 81019 dd59daa3c37a