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