src/HOL/Auth/Yahalom.ML
changeset 3500 0d8ad2f192d8
parent 3466 30791e5a69c4
child 3501 4ab477ffb4c6