src/HOL/Auth/KerberosIV.thy
changeset 32842 98702c579ad0
parent 32431 bcd14373ec30
child 32960 69916a850301