src/HOL/Code_Message.thy
changeset 29920 b95f5b8b93dd
parent 28952 15a4b2cf8c34
child 31032 38901ed00ec3