src/HOL/Tools/string_syntax.ML
changeset 28308 d4396a28fb29
parent 24712 64ed05609568
child 29317 9faf1dfb4e7c
equal deleted inserted replaced
28307:39328b6ea7e8 28308:d4396a28fb29