src/HOL/Auth/Guard/Extensions.thy
changeset 81303 cee03fbcec0d
parent 76289 a6cc15ec45b2