src/HOL/Auth/KerberosIV.thy
changeset 20751 93271c59d211
parent 18886 9f27383426db
child 20768 1d478c2d621f