src/HOL/Auth/KerberosV.thy
changeset 21522 bd641d927437
parent 21404 eb85850d3eb7
child 23746 a455e69c31cc
equal deleted inserted replaced
21521:095f4963beed 21522:bd641d927437