src/HOL/Auth/KerberosIV.thy
changeset 15572 9c89b1adf573
parent 14945 7bfe4fa8a88f
child 16417 9bc16273c2d4