src/HOL/Auth/Guard/Guard_Public.thy
changeset 17157 c5fb1fb537c0
parent 16417 9bc16273c2d4
child 20217 25b068a99d2b