src/HOL/Auth/Kerberos_BAN.thy
changeset 5393 7299e531d481
parent 5053 75d20f367e94
child 5434 9b4bed3f394c