src/HOL/String.thy
changeset 58710 7216a10d69ba
parent 58310 91ea607a34d8
child 58822 90a5e981af3e
equal deleted inserted replaced
58709:efdc6c533bd3 58710:7216a10d69ba