src/HOL/Auth/Guard/GuardK.thy
changeset 29270 0eade173f77e
parent 27108 e447b3107696
child 35416 d8d7d1b785af