src/HOL/Auth/NS_Public.thy
changeset 17157 c5fb1fb537c0
parent 16417 9bc16273c2d4
child 23746 a455e69c31cc