src/HOL/Auth/KerberosIV_Gets.thy
changeset 37407 61dd8c145da7
parent 36866 426d5781bb25
child 37809 6c87cdad912d