src/HOL/Auth/Guard/Extensions.thy
changeset 14024 213dcc39358f
parent 13596 ee5f79b210c1
child 14306 1d40d90398eb