src/HOL/Auth/Guard/Extensions.thy
changeset 79881 098c770e03f5
parent 76289 a6cc15ec45b2