src/HOL/Auth/Message.thy
changeset 14600 ba51bc239716
parent 14200 d8598e24f8fa
child 15032 02aed07e01bf