src/HOL/Auth/KerberosIV.thy
changeset 15813 741978011e12
parent 14945 7bfe4fa8a88f
child 16417 9bc16273c2d4