src/HOL/Auth/Guard/Extensions.thy
changeset 17767 504acb86c9f5
parent 17689 a04b5b43625e
child 18557 60a0f9caa0a2