src/HOL/Auth/Auth_Public.thy
changeset 76684 3eda063a20a4
parent 65538 a39ef48fbee0