src/HOL/Auth/Public.thy
changeset 78888 95bbf9a576b3
parent 76290 64d29ebb7d3d
child 81248 8205db6977dd