src/HOL/Auth/Guard/Extensions.thy
changeset 40739 9c84b562620d
parent 39246 9e58f0499f57
child 41775 6214816d79d3