src/HOL/Auth/Guard/Extensions.thy
changeset 25795 216c8e70d804
parent 21404 eb85850d3eb7
child 26809 da662ff93503