src/HOL/String.thy
changeset 57354 ded92100ffd7
parent 57247 8191ccf6a1bd
child 57437 0baf08c075b9