src/HOL/Auth/Kerberos_BAN.thy
changeset 12759 5f4fb54bfaf9
parent 11704 3c50a2cd6f00
child 13507 febb8e5d2a9d