src/HOL/Tools/string_syntax.ML
changeset 33002 f3f02f36a3e2
parent 31048 ac146fc38b51
child 35115 446c5063e4fd
equal deleted inserted replaced
33001:82382652e5e7 33002:f3f02f36a3e2