src/HOL/String.thy
changeset 33566 1c62ac4ef6d1
parent 33237 565ad811db21
child 34886 873c31d9f10d