src/HOL/String.thy
changeset 37490 9de1add14bac
parent 36176 3fe7e97ccca8
child 37743 0a3fa8fbcdc5
equal deleted inserted replaced
37489:44e42d392c6e 37490:9de1add14bac