src/HOL/Auth/Guard/Extensions.thy
changeset 56166 9a241bc276cd
parent 55417 01fbfb60c33e
child 56681 e8d5d60d655e