src/HOL/Tools/string_syntax.ML
changeset 30518 07b45c1aa788
parent 29317 9faf1dfb4e7c
child 31048 ac146fc38b51
equal deleted inserted replaced
30517:51a39ed24c0f 30518:07b45c1aa788