src/HOL/Auth/Auth_Public.thy
changeset 68398 194fa3d2d6a4
parent 65538 a39ef48fbee0