src/HOL/Auth/KerberosV.thy
changeset 43658 0d96ec6ec33b
parent 43587 0dd418de22ce
child 47050 7be54568efa1
equal deleted inserted replaced
43657:537ea3846f64 43658:0d96ec6ec33b