src/HOL/Auth/Message.thy
changeset 14360 e654599b114e
parent 14200 d8598e24f8fa
child 15032 02aed07e01bf