src/HOL/Auth/Guard/Extensions.thy
changeset 18684 38d72231b41d
parent 18557 60a0f9caa0a2
child 19233 77ca20b0ed77