src/HOL/Auth/Message.ML
changeset 3895 b2463861c86a
parent 3730 6933d20f335f
child 3919 c036caebfc75
equal deleted inserted replaced
3894:8b9f0bc6dc1a 3895:b2463861c86a