src/HOL/Auth/Guard/GuardK.thy
changeset 47987 4e9df6ffcc6e
parent 45600 1bbbac9a0cb0
child 55417 01fbfb60c33e