src/HOL/Auth/Guard/Extensions.thy
changeset 21488 e1b260d204a0
parent 21404 eb85850d3eb7
child 26809 da662ff93503