src/HOL/Auth/KerberosIV.thy
changeset 19265 cae36e16f3c0
parent 18886 9f27383426db
child 20768 1d478c2d621f