src/HOL/Auth/Message.ML
changeset 8042 ecdedff41e67
parent 7057 b9ddbb925939
child 8054 2ce57ef2a4aa
equal deleted inserted replaced
8041:e3237d8c18d6 8042:ecdedff41e67