src/HOL/Auth/Message_lemmas.ML
changeset 13028 81c87faed78b
parent 11270 a315a3862bb4