src/HOL/Auth/Message.ML
changeset 2250 891eb76b8045
parent 2170 c5e460f1ebb4
child 2284 80ebd1a213fd