src/HOL/Auth/Kerberos_BAN.thy
changeset 7165 8c937127fd8c
parent 5434 9b4bed3f394c
child 11185 1b737b4c2108
equal deleted inserted replaced
7164:295882e50b7a 7165:8c937127fd8c