src/HOL/Auth/Message.thy
changeset 11566 94d2d6531c57
parent 11270 a315a3862bb4
child 13922 75ae4244a596