src/HOL/Auth/Event.ML
changeset 3659 eddedfe2f3f8
parent 3519 ab0a9fbed4c0
child 3667 42a726e008ce