src/HOL/Tools/string_syntax.ML
changeset 82845 d4da7d857bb7
parent 81019 dd59daa3c37a
equal deleted inserted replaced
82844:ebfb0e011c95 82845:d4da7d857bb7