src/HOL/Auth/Kerberos_BAN.ML
changeset 8364 0eb9ee70c8f8
parent 7499 23e090051cb8
child 8741 61bc5ed22b62