src/HOL/Auth/Message.thy
changeset 13145 59bc43b51aa2
parent 11270 a315a3862bb4
child 13922 75ae4244a596