src/HOL/Auth/Kerberos_BAN.thy
changeset 40255 9ffbc25e1606
parent 39251 8756b44582e2
child 42749 47f283fcf2ae
equal deleted inserted replaced
40254:6d1ebaa7a4ba 40255:9ffbc25e1606