src/HOL/Auth/Message.ML
changeset 11188 5d539f1682c3
parent 11150 67387142225e