src/HOL/Auth/KerberosIV.thy
changeset 11837 b2a9853ec6dd
parent 11704 3c50a2cd6f00
child 13507 febb8e5d2a9d