src/HOL/Auth/KerberosIV_Gets.thy
changeset 26140 e45375135052
parent 23746 a455e69c31cc
child 26301 28193aedc718