src/HOL/Auth/Message.thy
changeset 60592 c9bd1d902f04
parent 59780 23b67731f4f0
child 61830 4f5ab843cf5b