src/HOL/Auth/Guard/Extensions.thy
changeset 26864 1417e704d724
parent 26809 da662ff93503
child 32695 66ae4e8b1309