src/HOL/Auth/Event_lemmas.ML
changeset 13605 528f7489a403
parent 12415 74977582a585