src/HOL/String.thy
changeset 33689 d0a9ce721e0c
parent 33237 565ad811db21
child 34886 873c31d9f10d
equal deleted inserted replaced
33688:1a97dcd8dc6a 33689:d0a9ce721e0c