src/HOL/Auth/Guard/GuardK.thy
changeset 17307 a6d206750d6d
parent 17087 0abf74bdf712
child 19233 77ca20b0ed77