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