src/HOL/Auth/KerberosV.thy
changeset 74926 5cd2e6e17e6f
parent 69597 ff784d5a5bfb
child 76290 64d29ebb7d3d
equal deleted inserted replaced
74918:68a0f9a8561d 74926:5cd2e6e17e6f