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