src/HOL/Tools/string_syntax.ML
changeset 32318 bca7fd849829
parent 31048 ac146fc38b51
child 35115 446c5063e4fd
equal deleted inserted replaced
32317:b4b871808223 32318:bca7fd849829