src/HOL/Auth/Guard/Extensions.thy
changeset 72118 84f716e72fa3
parent 69597 ff784d5a5bfb
child 76287 cdc14f94c754