src/HOL/Auth/Kerberos_BAN.thy
changeset 33779 b8efeea2cebd
parent 32960 69916a850301
child 36866 426d5781bb25
equal deleted inserted replaced
33778:9121ea165a40 33779:b8efeea2cebd