src/HOL/Auth/KerberosIV.thy
changeset 34195 d58da36d1a30
parent 33304 2c77579e0523
child 35416 d8d7d1b785af