src/HOL/Auth/Guard/Guard.thy
changeset 24077 e7ba448bc571
parent 23746 a455e69c31cc
child 25134 3d4953e88449