src/HOL/Code_Message.thy
changeset 29127 2a684ee023e7
parent 28952 15a4b2cf8c34
child 31032 38901ed00ec3