src/HOL/Auth/KerberosV.thy
changeset 46138 85f8d8a8c711
parent 43587 0dd418de22ce
child 47050 7be54568efa1