src/HOL/Auth/Public.thy
changeset 20192 956cd30ef3be
parent 20048 a7964311f1fb
child 20768 1d478c2d621f