src/HOL/Auth/Public.thy
changeset 14360 e654599b114e
parent 14261 6c418d139f74
child 15032 02aed07e01bf