src/HOL/Auth/KerberosIV.thy
changeset 20205 7b2958d3d575
parent 18886 9f27383426db
child 20768 1d478c2d621f