src/HOL/String.thy
changeset 72139 f5c085dfa02f
parent 72024 9b4135e8bade
child 72164 b7c54ff7f2dd