src/HOL/Auth/KerberosIV.thy
changeset 12791 ccc0f45ad2c4
parent 11704 3c50a2cd6f00
child 13507 febb8e5d2a9d