src/HOL/Auth/Kerberos_BAN.ML
changeset 5242 3087dafb70ec
parent 5223 4cb05273f764
child 5352 a32312d17ed6
equal deleted inserted replaced
5241:e5129172cb2b 5242:3087dafb70ec