src/HOL/String.thy
changeset 70759 26837fd025a3
parent 70340 7383930fc946
child 71094 a197532693a5