src/HOL/Auth/Message.ML
changeset 6427 fd36b2e7d80e
parent 6141 a6922171b396
child 6915 4ab8e31a8421