src/HOL/Auth/Guard/Extensions.thy
changeset 17220 b41d8e290bf8
parent 16417 9bc16273c2d4
child 17689 a04b5b43625e