src/HOL/Auth/KerberosIV_Gets.thy
changeset 28957 da6c224a06e6
parent 26301 28193aedc718
child 32960 69916a850301
equal deleted inserted replaced
28956:64754369cee3 28957:da6c224a06e6