src/HOL/Auth/Kerberos_BAN_Gets.thy
changeset 39564 acfd10e38e80
parent 39251 8756b44582e2
child 44890 22f665a2e91c