src/HOL/Auth/KerberosV.thy
changeset 32379 a97e9caebd60
parent 26300 03def556e26e
child 32404 da3ca3c6ec81