src/HOL/Auth/Guard/Extensions.thy
changeset 21984 7b9c2f6b45f5
parent 21404 eb85850d3eb7
child 26809 da662ff93503