src/HOL/Auth/Guard/Extensions.thy
changeset 31106 9a1178204dc0
parent 26809 da662ff93503
child 32695 66ae4e8b1309