src/HOL/Tools/string_syntax.ML
changeset 80946 b76f64d7d493
parent 80795 5e38e8b34eb3
child 81019 dd59daa3c37a