src/HOL/Auth/KerberosIV_Gets.thy
changeset 81151 0d728eadad86
parent 80914 d97fdabd9e2b