src/HOL/Auth/KerberosIV.thy
changeset 13343 3b2b18c58d80
parent 11704 3c50a2cd6f00
child 13507 febb8e5d2a9d