src/HOL/Auth/Message_lemmas.ML
changeset 13605 528f7489a403
parent 11270 a315a3862bb4