src/HOL/Auth/KerberosV.thy
changeset 28957 da6c224a06e6
parent 26300 03def556e26e
child 32404 da3ca3c6ec81
equal deleted inserted replaced
28956:64754369cee3 28957:da6c224a06e6