src/HOL/Auth/Event_lemmas.ML
changeset 13352 3cd767f8d78b
parent 12415 74977582a585