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