src/HOL/Code_Message.thy
changeset 29578 8c4e961fcb08
parent 28952 15a4b2cf8c34
child 31032 38901ed00ec3