src/HOL/Auth/Message.thy
changeset 14706 71590b7733b7
parent 14200 d8598e24f8fa
child 15032 02aed07e01bf