src/HOL/Auth/Public.thy
changeset 15341 254f6f00b60e
parent 15032 02aed07e01bf
child 15616 cdf6eeb4ac27