src/HOL/Auth/Auth_Public.thy
changeset 80182 29f2b8ff84f3
parent 65538 a39ef48fbee0