src/HOL/Auth/Yahalom.ML
changeset 2448 61337170db84
parent 2377 ad9d2dedaeaa
child 2451 ce85a2aafc7a