src/HOL/String.thy
changeset 81017 bc5eb7841b74
parent 80932 261cd8722677
child 81113 6fefd6c602fa