src/HOL/Auth/KerberosIV_Gets.thy
changeset 31038 887298ab70dc
parent 26301 28193aedc718
child 32960 69916a850301