src/HOL/Auth/KerberosIV.thy
changeset 21205 dfe338ec9f9c
parent 20768 1d478c2d621f
child 21404 eb85850d3eb7
equal deleted inserted replaced
21204:1e96553668c6 21205:dfe338ec9f9c