src/HOL/Auth/Guard/Extensions.thy
changeset 23092 f3615235dc4d
parent 21404 eb85850d3eb7
child 26809 da662ff93503