src/HOL/Auth/Message.thy
changeset 53147 8e8941fea278
parent 51717 9e7d1c139569
child 57394 7621a3b42ce7