src/HOL/String.thy
changeset 67316 adaf279ce67b
parent 67091 1393c2340eec
child 67399 eab6ce8368fa