src/HOL/String.thy
changeset 70421 617cd75fc3de
parent 70340 7383930fc946
child 71094 a197532693a5