src/HOL/Auth/Kerberos_BAN_Gets.thy
changeset 35266 07a56610c00b
parent 32960 69916a850301
child 36866 426d5781bb25