src/HOL/Auth/KerberosIV.ML
changeset 8740 fa6c4e4182d9
parent 7499 23e090051cb8
child 8741 61bc5ed22b62