src/HOL/Auth/Kerberos_BAN_Gets.thy
changeset 27573 10ba0d7d94e0
parent 23746 a455e69c31cc
child 32960 69916a850301
equal deleted inserted replaced
27572:67cd6ed76446 27573:10ba0d7d94e0